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  1872  mor  2087  ceqsalg  2791  cgsexg  2798  cgsex2g  2799  cgsex4g  2800  spc2egv  2854  spc2gv  2855  spc3egv  2856  spc3gv  2857  disjne  3504  uneqdifeqim  3536  eqifdc  3596  triun  4144  sucssel  4459  ordsucg  4538  regexmidlem1  4569  relresfld  5199  relcoi1  5201  focdmex  6172  f1dmex  6173  dom2d  6832  findcard  6949  nneo  9429  zeo2  9432  uznfz  10178  difelfzle  10209  ssfzo12  10300  facndiv  10831  fisumcom2  11603  fprodssdc  11755  fprodcom2fi  11791  ndvdssub  12095  bezoutlembi  12172  eucalglt  12225  prmind2  12288  coprm  12312  prmdiveq  12404  mhmlin  13099  issubg2m  13319  nsgbi  13334  issubrng2  13766  issubrg2  13797  lmodlema  13848  rmodislmodlem  13906  rmodislmod  13907  lspsnel6  13964  inopn  14239  basis1  14283  tgss  14299  tgcl  14300  xmeteq0  14595  blssexps  14665  blssex  14666  mopni3  14720  neibl  14727  metss  14730  metcnp3  14747  logbgcd1irr  15203  gausslemma2dlem0i  15298  2lgsoddprmlem3  15352  bj-indsuc  15574  bj-nntrans  15597