Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical implication
sylcom
Metamath Proof Explorer
Description: Syllogism inference with commutation of antecedents. (Contributed by NM , 29-Aug-2004) (Proof shortened by Mel L. O'Cat , 2-Feb-2006)
(Proof shortened by Stefan Allan , 23-Feb-2006)

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

Proof
Step
Hyp
Ref
Expression
1
sylcom.1
$${\u22a2}{\phi}\to \left({\psi}\to {\chi}\right)$$
2
sylcom.2
$${\u22a2}{\psi}\to \left({\chi}\to {\theta}\right)$$
3
2
a2i
$${\u22a2}\left({\psi}\to {\chi}\right)\to \left({\psi}\to {\theta}\right)$$
4
1 3
syl
$${\u22a2}{\phi}\to \left({\psi}\to {\theta}\right)$$