Artificial intelligent assistant

How are statements laid out in deductive proof? so I am doing deductive proof, I know this contains a lot of laws that you need to be familiar with. And I have all that I need here. However, I don't known when to use more than one premise. For example say: ## * * * 1: A ⇒ B Premise 2: C ⇒ D Premise 3: B ∨ D ⇒ E Premise 4: ¬E Premise 5: ¬(B ∨ D) **from 3 & 4 modus tollens** Here what I don't understand is when it says 3 & 4 modus tollens, How is 3 & 4 actually laid out before applying modus tollens? Also the modus tollens rule says: ¬p ∧ (p ⇒ q) ⇒ ¬p So how can it be applied to 3 & 4?

Obviously, in a derivation, when we apply a _rule_ , this rule must use (one or more) formulas already present in the derivation.

Thus, if we refer to lines in the derivation by numbers, the simple rule must be:

> in line $n$ apply _Rule X_ to formulas in lines $i$ and $j$, with $i,j < n$.

With Modus tollens we can refer either to a _rule_ :

> $P\to Q,\lnot Q\vdash \lnot P$,

or to a _tautology_ :

> $((P\to Q)\land \
eg Q)\to \
eg P$.

In the first case, your line 5 is fine: it follows from lines 3) and 4) by _MT_.

In the second case, to be "formal", we have to interpose some intermediate steps :

> 4') $((B \lor D) \to E)\land \
eg E$ --- from 3) and 4) by Conjunction
>
> 4'') $[((B \lor D) \to E)\land \
eg E] \to \
eg ((B \lor D) \to E)$ --- tautology : _Modus Tollens_

to get :

> > 5) $\
eg (B \lor D) \to E$ --- from 4') and 4'') by _Modus ponens_.

xcX3v84RxoQ-4GxG32940ukFUIEgYdPy d1faaf1efe26f4f87624e6b2a69dc952