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  874  pm5.11dc  921  ax16i  1911  mor  2129  ceqsalg  2850  cgsexg  2857  cgsex2g  2858  cgsex4g  2859  spc2egv  2915  spc2gv  2916  spc3egv  2917  spc3gv  2918  disjne  3578  uneqdifeqim  3613  eqifdc  3677  triun  4240  sucssel  4567  ordsucg  4647  regexmidlem1  4678  relresfld  5315  relcoi1  5317  focdmex  6338  f1dmex  6339  dom2d  7053  findcard  7186  nneo  9732  zeo2  9735  uznfz  10493  difelfzle  10524  ssfzo12  10625  facndiv  11160  swrdswrd  11460  pfxccatin12lem2  11486  pfxccatin12  11488  pfxccat3  11489  fisumcom2  12188  fprodssdc  12340  fprodcom2fi  12376  ndvdssub  12680  bezoutlembi  12765  eucalglt  12818  prmind2  12881  coprm  12905  prmdiveq  12997  mhmlin  13757  issubg2m  13975  nsgbi  13990  issubrng2  14501  issubrg2  14532  lmodlema  14611  rmodislmodlem  14670  rmodislmod  14671  ellspsn6  14728  inopn  15087  basis1  15131  tgss  15147  tgcl  15148  xmeteq0  15443  blssexps  15513  blssex  15514  mopni3  15568  neibl  15575  metss  15578  metcnp3  15595  logbgcd1irr  16052  gausslemma2dlem0i  16159  2lgsoddprmlem3  16213  clwwlkn1loopb  16644  clwwlknonex2lem2  16662  bj-indsuc  16937  bj-nntrans  16960