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  852  pm5.11dc  899  ax16i  1846  mor  2056  ceqsalg  2754  cgsexg  2761  cgsex2g  2762  cgsex4g  2763  spc2egv  2816  spc2gv  2817  spc3egv  2818  spc3gv  2819  disjne  3462  uneqdifeqim  3494  eqifdc  3554  triun  4093  sucssel  4402  ordsucg  4479  regexmidlem1  4510  relresfld  5133  relcoi1  5135  fornex  6083  f1dmex  6084  dom2d  6739  findcard  6854  nneo  9294  zeo2  9297  uznfz  10038  difelfzle  10069  ssfzo12  10159  facndiv  10652  fisumcom2  11379  fprodssdc  11531  fprodcom2fi  11567  ndvdssub  11867  bezoutlembi  11938  eucalglt  11989  prmind2  12052  coprm  12076  prmdiveq  12168  inopn  12651  basis1  12695  tgss  12713  tgcl  12714  xmeteq0  13009  blssexps  13079  blssex  13080  mopni3  13134  neibl  13141  metss  13144  metcnp3  13161  logbgcd1irr  13535  bj-indsuc  13820  bj-nntrans  13843