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  793  pm5.11dc  849  ax16i  1781  mor  1985  ceqsalg  2636  cgsexg  2643  cgsex2g  2644  cgsex4g  2645  spc2egv  2696  spc2gv  2697  spc3egv  2698  spc3gv  2699  disjne  3313  uneqdifeqim  3344  triun  3908  sucssel  4207  ordsucg  4274  regexmidlem1  4304  relresfld  4897  relcoi1  4899  fornex  5793  f1dmex  5794  dom2d  6341  findcard  6444  nneo  8583  zeo2  8586  uznfz  9248  difelfzle  9274  ssfzo12  9362  facndiv  9815  ndvdssub  10537  bezoutlembi  10601  eucalglt  10646  prmind2  10709  coprm  10730  bj-indsuc  10990  bj-nntrans  11013