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  847  pm5.11dc  894  ax16i  1830  mor  2041  ceqsalg  2714  cgsexg  2721  cgsex2g  2722  cgsex4g  2723  spc2egv  2775  spc2gv  2776  spc3egv  2777  spc3gv  2778  disjne  3416  uneqdifeqim  3448  eqifdc  3506  triun  4039  sucssel  4346  ordsucg  4418  regexmidlem1  4448  relresfld  5068  relcoi1  5070  fornex  6013  f1dmex  6014  dom2d  6667  findcard  6782  nneo  9154  zeo2  9157  uznfz  9883  difelfzle  9911  ssfzo12  10001  facndiv  10485  fisumcom2  11207  ndvdssub  11627  bezoutlembi  11693  eucalglt  11738  prmind2  11801  coprm  11822  inopn  12170  basis1  12214  tgss  12232  tgcl  12233  xmeteq0  12528  blssexps  12598  blssex  12599  mopni3  12653  neibl  12660  metss  12663  metcnp3  12680  bj-indsuc  13126  bj-nntrans  13149