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  4516  ordsucg  4595  regexmidlem1  4626  relresfld  5261  relcoi1  5263  focdmex  6269  f1dmex  6270  dom2d  6937  findcard  7063  nneo  9566  zeo2  9569  uznfz  10316  difelfzle  10347  ssfzo12  10447  facndiv  10978  swrdswrd  11258  pfxccatin12lem2  11284  pfxccatin12  11286  pfxccat3  11287  fisumcom2  11970  fprodssdc  12122  fprodcom2fi  12158  ndvdssub  12462  bezoutlembi  12547  eucalglt  12600  prmind2  12663  coprm  12687  prmdiveq  12779  mhmlin  13521  issubg2m  13747  nsgbi  13762  issubrng2  14195  issubrg2  14226  lmodlema  14277  rmodislmodlem  14335  rmodislmod  14336  lspsnel6  14393  inopn  14698  basis1  14742  tgss  14758  tgcl  14759  xmeteq0  15054  blssexps  15124  blssex  15125  mopni3  15179  neibl  15186  metss  15189  metcnp3  15206  logbgcd1irr  15662  gausslemma2dlem0i  15757  2lgsoddprmlem3  15811  clwwlkn1loopb  16188  bj-indsuc  16400  bj-nntrans  16423