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  867  pm5.11dc  914  ax16i  1904  mor  2120  ceqsalg  2829  cgsexg  2836  cgsex2g  2837  cgsex4g  2838  spc2egv  2894  spc2gv  2895  spc3egv  2896  spc3gv  2897  disjne  3546  uneqdifeqim  3578  eqifdc  3640  triun  4198  sucssel  4519  ordsucg  4598  regexmidlem1  4629  relresfld  5264  relcoi1  5266  focdmex  6272  f1dmex  6273  dom2d  6941  findcard  7072  nneo  9576  zeo2  9579  uznfz  10331  difelfzle  10362  ssfzo12  10462  facndiv  10994  swrdswrd  11279  pfxccatin12lem2  11305  pfxccatin12  11307  pfxccat3  11308  fisumcom2  11992  fprodssdc  12144  fprodcom2fi  12180  ndvdssub  12484  bezoutlembi  12569  eucalglt  12622  prmind2  12685  coprm  12709  prmdiveq  12801  mhmlin  13543  issubg2m  13769  nsgbi  13784  issubrng2  14217  issubrg2  14248  lmodlema  14299  rmodislmodlem  14357  rmodislmod  14358  lspsnel6  14415  inopn  14720  basis1  14764  tgss  14780  tgcl  14781  xmeteq0  15076  blssexps  15146  blssex  15147  mopni3  15201  neibl  15208  metss  15211  metcnp3  15228  logbgcd1irr  15684  gausslemma2dlem0i  15779  2lgsoddprmlem3  15833  clwwlkn1loopb  16229  clwwlknonex2lem2  16247  bj-indsuc  16473  bj-nntrans  16496