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-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  com12  30  syl5  32  pm2.6dc  862  pm5.11dc  909  ax16i  1858  mor  2068  ceqsalg  2766  cgsexg  2773  cgsex2g  2774  cgsex4g  2775  spc2egv  2828  spc2gv  2829  spc3egv  2830  spc3gv  2831  disjne  3477  uneqdifeqim  3509  eqifdc  3570  triun  4115  sucssel  4425  ordsucg  4502  regexmidlem1  4533  relresfld  5159  relcoi1  5161  focdmex  6116  f1dmex  6117  dom2d  6773  findcard  6888  nneo  9356  zeo2  9359  uznfz  10103  difelfzle  10134  ssfzo12  10224  facndiv  10719  fisumcom2  11446  fprodssdc  11598  fprodcom2fi  11634  ndvdssub  11935  bezoutlembi  12006  eucalglt  12057  prmind2  12120  coprm  12144  prmdiveq  12236  mhmlin  12858  issubg2m  13049  nsgbi  13064  issubrg2  13362  lmodlema  13382  rmodislmodlem  13440  rmodislmod  13441  inopn  13506  basis1  13550  tgss  13566  tgcl  13567  xmeteq0  13862  blssexps  13932  blssex  13933  mopni3  13987  neibl  13994  metss  13997  metcnp3  14014  logbgcd1irr  14388  2lgsoddprmlem3  14462  bj-indsuc  14683  bj-nntrans  14706