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  870  pm5.11dc  917  ax16i  1907  mor  2125  ceqsalg  2844  cgsexg  2851  cgsex2g  2852  cgsex4g  2853  spc2egv  2909  spc2gv  2910  spc3egv  2911  spc3gv  2912  disjne  3566  uneqdifeqim  3599  eqifdc  3663  triun  4226  sucssel  4550  ordsucg  4629  regexmidlem1  4660  relresfld  5297  relcoi1  5299  focdmex  6317  f1dmex  6318  dom2d  7025  findcard  7158  nneo  9699  zeo2  9702  uznfz  10459  difelfzle  10490  ssfzo12  10591  facndiv  11126  swrdswrd  11422  pfxccatin12lem2  11448  pfxccatin12  11450  pfxccat3  11451  fisumcom2  12149  fprodssdc  12301  fprodcom2fi  12337  ndvdssub  12641  bezoutlembi  12726  eucalglt  12779  prmind2  12842  coprm  12866  prmdiveq  12958  mhmlin  13764  issubg2m  13990  nsgbi  14005  issubrng2  14441  issubrg2  14472  lmodlema  14552  rmodislmodlem  14610  rmodislmod  14611  lspsnel6  14668  inopn  14980  basis1  15024  tgss  15040  tgcl  15041  xmeteq0  15336  blssexps  15406  blssex  15407  mopni3  15461  neibl  15468  metss  15471  metcnp3  15488  logbgcd1irr  15944  gausslemma2dlem0i  16042  2lgsoddprmlem3  16096  clwwlkn1loopb  16527  clwwlknonex2lem2  16545  bj-indsuc  16810  bj-nntrans  16833