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  2828  cgsexg  2835  cgsex2g  2836  cgsex4g  2837  spc2egv  2893  spc2gv  2894  spc3egv  2895  spc3gv  2896  disjne  3545  uneqdifeqim  3577  eqifdc  3639  triun  4195  sucssel  4515  ordsucg  4594  regexmidlem1  4625  relresfld  5258  relcoi1  5260  focdmex  6266  f1dmex  6267  dom2d  6932  findcard  7058  nneo  9558  zeo2  9561  uznfz  10307  difelfzle  10338  ssfzo12  10438  facndiv  10969  swrdswrd  11245  pfxccatin12lem2  11271  pfxccatin12  11273  pfxccat3  11274  fisumcom2  11957  fprodssdc  12109  fprodcom2fi  12145  ndvdssub  12449  bezoutlembi  12534  eucalglt  12587  prmind2  12650  coprm  12674  prmdiveq  12766  mhmlin  13508  issubg2m  13734  nsgbi  13749  issubrng2  14182  issubrg2  14213  lmodlema  14264  rmodislmodlem  14322  rmodislmod  14323  lspsnel6  14380  inopn  14685  basis1  14729  tgss  14745  tgcl  14746  xmeteq0  15041  blssexps  15111  blssex  15112  mopni3  15166  neibl  15173  metss  15176  metcnp3  15193  logbgcd1irr  15649  gausslemma2dlem0i  15744  2lgsoddprmlem3  15798  bj-indsuc  16315  bj-nntrans  16338