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  857  pm5.11dc  904  ax16i  1851  mor  2061  ceqsalg  2758  cgsexg  2765  cgsex2g  2766  cgsex4g  2767  spc2egv  2820  spc2gv  2821  spc3egv  2822  spc3gv  2823  disjne  3468  uneqdifeqim  3500  eqifdc  3560  triun  4100  sucssel  4409  ordsucg  4486  regexmidlem1  4517  relresfld  5140  relcoi1  5142  fornex  6094  f1dmex  6095  dom2d  6751  findcard  6866  nneo  9315  zeo2  9318  uznfz  10059  difelfzle  10090  ssfzo12  10180  facndiv  10673  fisumcom2  11401  fprodssdc  11553  fprodcom2fi  11589  ndvdssub  11889  bezoutlembi  11960  eucalglt  12011  prmind2  12074  coprm  12098  prmdiveq  12190  mhmlin  12690  inopn  12795  basis1  12839  tgss  12857  tgcl  12858  xmeteq0  13153  blssexps  13223  blssex  13224  mopni3  13278  neibl  13285  metss  13288  metcnp3  13305  logbgcd1irr  13679  bj-indsuc  13963  bj-nntrans  13986