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  863  pm5.11dc  910  ax16i  1872  mor  2087  ceqsalg  2791  cgsexg  2798  cgsex2g  2799  cgsex4g  2800  spc2egv  2854  spc2gv  2855  spc3egv  2856  spc3gv  2857  disjne  3505  uneqdifeqim  3537  eqifdc  3597  triun  4145  sucssel  4460  ordsucg  4539  regexmidlem1  4570  relresfld  5200  relcoi1  5202  focdmex  6181  f1dmex  6182  dom2d  6841  findcard  6958  nneo  9448  zeo2  9451  uznfz  10197  difelfzle  10228  ssfzo12  10319  facndiv  10850  fisumcom2  11622  fprodssdc  11774  fprodcom2fi  11810  ndvdssub  12114  bezoutlembi  12199  eucalglt  12252  prmind2  12315  coprm  12339  prmdiveq  12431  mhmlin  13171  issubg2m  13397  nsgbi  13412  issubrng2  13844  issubrg2  13875  lmodlema  13926  rmodislmodlem  13984  rmodislmod  13985  lspsnel6  14042  inopn  14347  basis1  14391  tgss  14407  tgcl  14408  xmeteq0  14703  blssexps  14773  blssex  14774  mopni3  14828  neibl  14835  metss  14838  metcnp3  14855  logbgcd1irr  15311  gausslemma2dlem0i  15406  2lgsoddprmlem3  15460  bj-indsuc  15682  bj-nntrans  15705