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  4194  sucssel  4512  ordsucg  4591  regexmidlem1  4622  relresfld  5254  relcoi1  5256  focdmex  6250  f1dmex  6251  dom2d  6914  findcard  7038  nneo  9538  zeo2  9541  uznfz  10287  difelfzle  10318  ssfzo12  10417  facndiv  10948  swrdswrd  11223  pfxccatin12lem2  11249  pfxccatin12  11251  pfxccat3  11252  fisumcom2  11935  fprodssdc  12087  fprodcom2fi  12123  ndvdssub  12427  bezoutlembi  12512  eucalglt  12565  prmind2  12628  coprm  12652  prmdiveq  12744  mhmlin  13486  issubg2m  13712  nsgbi  13727  issubrng2  14159  issubrg2  14190  lmodlema  14241  rmodislmodlem  14299  rmodislmod  14300  lspsnel6  14357  inopn  14662  basis1  14706  tgss  14722  tgcl  14723  xmeteq0  15018  blssexps  15088  blssex  15089  mopni3  15143  neibl  15150  metss  15153  metcnp3  15170  logbgcd1irr  15626  gausslemma2dlem0i  15721  2lgsoddprmlem3  15775  bj-indsuc  16221  bj-nntrans  16244