Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical implication
syl5d
Metamath Proof Explorer
Description: A nested syllogism deduction. Deduction associated with syl5 .
(Contributed by NM , 14-May-1993) (Proof shortened by Josh Purinton , 29-Dec-2000) (Proof shortened by Mel L. O'Cat , 2-Feb-2006)

Ref
Expression
Hypotheses
syl5d.1
$${\u22a2}{\phi}\to \left({\psi}\to {\chi}\right)$$
syl5d.2
$${\u22a2}{\phi}\to \left({\theta}\to \left({\chi}\to {\tau}\right)\right)$$
Assertion
syl5d
$${\u22a2}{\phi}\to \left({\theta}\to \left({\psi}\to {\tau}\right)\right)$$

Proof
Step
Hyp
Ref
Expression
1
syl5d.1
$${\u22a2}{\phi}\to \left({\psi}\to {\chi}\right)$$
2
syl5d.2
$${\u22a2}{\phi}\to \left({\theta}\to \left({\chi}\to {\tau}\right)\right)$$
3
1
a1d
$${\u22a2}{\phi}\to \left({\theta}\to \left({\psi}\to {\chi}\right)\right)$$
4
3 2
syldd
$${\u22a2}{\phi}\to \left({\theta}\to \left({\psi}\to {\tau}\right)\right)$$