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  9702  zeo2  9705  uznfz  10462  difelfzle  10493  ssfzo12  10594  facndiv  11129  swrdswrd  11425  pfxccatin12lem2  11451  pfxccatin12  11453  pfxccat3  11454  fisumcom2  12153  fprodssdc  12305  fprodcom2fi  12341  ndvdssub  12645  bezoutlembi  12730  eucalglt  12783  prmind2  12846  coprm  12870  prmdiveq  12962  mhmlin  13726  issubg2m  13946  nsgbi  13961  issubrng2  14460  issubrg2  14491  lmodlema  14570  rmodislmodlem  14628  rmodislmod  14629  lspsnel6  14686  inopn  14998  basis1  15042  tgss  15058  tgcl  15059  xmeteq0  15354  blssexps  15424  blssex  15425  mopni3  15479  neibl  15486  metss  15489  metcnp3  15506  logbgcd1irr  15962  gausslemma2dlem0i  16060  2lgsoddprmlem3  16114  clwwlkn1loopb  16545  clwwlknonex2lem2  16563  bj-indsuc  16838  bj-nntrans  16861