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  6174  f1dmex  6175  dom2d  6834  findcard  6951  nneo  9432  zeo2  9435  uznfz  10181  difelfzle  10212  ssfzo12  10303  facndiv  10834  fisumcom2  11606  fprodssdc  11758  fprodcom2fi  11794  ndvdssub  12098  bezoutlembi  12183  eucalglt  12236  prmind2  12299  coprm  12323  prmdiveq  12415  mhmlin  13125  issubg2m  13345  nsgbi  13360  issubrng2  13792  issubrg2  13823  lmodlema  13874  rmodislmodlem  13932  rmodislmod  13933  lspsnel6  13990  inopn  14265  basis1  14309  tgss  14325  tgcl  14326  xmeteq0  14621  blssexps  14691  blssex  14692  mopni3  14746  neibl  14753  metss  14756  metcnp3  14773  logbgcd1irr  15229  gausslemma2dlem0i  15324  2lgsoddprmlem3  15378  bj-indsuc  15600  bj-nntrans  15623