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  863  pm5.11dc  910  ax16i  1869  mor  2084  ceqsalg  2788  cgsexg  2795  cgsex2g  2796  cgsex4g  2797  spc2egv  2851  spc2gv  2852  spc3egv  2853  spc3gv  2854  disjne  3501  uneqdifeqim  3533  eqifdc  3593  triun  4141  sucssel  4456  ordsucg  4535  regexmidlem1  4566  relresfld  5196  relcoi1  5198  focdmex  6169  f1dmex  6170  dom2d  6829  findcard  6946  nneo  9423  zeo2  9426  uznfz  10172  difelfzle  10203  ssfzo12  10294  facndiv  10813  fisumcom2  11584  fprodssdc  11736  fprodcom2fi  11772  ndvdssub  12074  bezoutlembi  12145  eucalglt  12198  prmind2  12261  coprm  12285  prmdiveq  12377  mhmlin  13042  issubg2m  13262  nsgbi  13277  issubrng2  13709  issubrg2  13740  lmodlema  13791  rmodislmodlem  13849  rmodislmod  13850  lspsnel6  13907  inopn  14182  basis1  14226  tgss  14242  tgcl  14243  xmeteq0  14538  blssexps  14608  blssex  14609  mopni3  14663  neibl  14670  metss  14673  metcnp3  14690  logbgcd1irr  15140  gausslemma2dlem0i  15214  2lgsoddprmlem3  15268  bj-indsuc  15490  bj-nntrans  15513