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  1906  mor  2122  ceqsalg  2832  cgsexg  2839  cgsex2g  2840  cgsex4g  2841  spc2egv  2897  spc2gv  2898  spc3egv  2899  spc3gv  2900  disjne  3550  uneqdifeqim  3582  eqifdc  3646  triun  4205  sucssel  4527  ordsucg  4606  regexmidlem1  4637  relresfld  5273  relcoi1  5275  focdmex  6286  f1dmex  6287  dom2d  6989  findcard  7120  nneo  9626  zeo2  9629  uznfz  10381  difelfzle  10412  ssfzo12  10513  facndiv  11045  swrdswrd  11333  pfxccatin12lem2  11359  pfxccatin12  11361  pfxccat3  11362  fisumcom2  12060  fprodssdc  12212  fprodcom2fi  12248  ndvdssub  12552  bezoutlembi  12637  eucalglt  12690  prmind2  12753  coprm  12777  prmdiveq  12869  mhmlin  13611  issubg2m  13837  nsgbi  13852  issubrng2  14286  issubrg2  14317  lmodlema  14368  rmodislmodlem  14426  rmodislmod  14427  lspsnel6  14484  inopn  14794  basis1  14838  tgss  14854  tgcl  14855  xmeteq0  15150  blssexps  15220  blssex  15221  mopni3  15275  neibl  15282  metss  15285  metcnp3  15302  logbgcd1irr  15758  gausslemma2dlem0i  15856  2lgsoddprmlem3  15910  clwwlkn1loopb  16341  clwwlknonex2lem2  16359  bj-indsuc  16624  bj-nntrans  16647