Theorem syl5com 29

Description: Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.)

Hypotheses

Ref	Expression
syl5com.1	⊢ (𝜑 → 𝜓)
syl5com.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
syl5com	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem syl5com

Step	Hyp	Ref	Expression
1		syl5com.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1d 22	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
3		syl5com.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	sylcom 28	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  com12  30  syl5  32  pm2.6dc  792  pm5.11dc  848  ax16i  1779  mor  1983  ceqsalg  2627  cgsexg  2634  cgsex2g  2635  cgsex4g  2636  spc2egv  2687  spc2gv  2688  spc3egv  2689  spc3gv  2690  disjne  3297  uneqdifeqim  3328  triun  3888  sucssel  4179  ordsucg  4246  regexmidlem1  4276  relresfld  4867  relcoi1  4869  fornex  5762  f1dmex  5763  rdgon  5996  dom2d  6276  findcard  6372  nneo  8450  zeo2  8453  uznfz  9120  difelfzle  9145  ssfzo12  9233  facndiv  9666  ndvdssub  10330  bezoutlembi  10394  eucalglt  10439  prmind2  10502  coprm  10523  bj-indsuc  10723  bj-nntrans  10746