Theorem sylcom 31

Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 29-Aug-2004.) (Proof shortened by Mel L. O'Cat, 2-Feb-2006.) (Proof shortened by Stefan Allan, 23-Feb-2006.)

Hypotheses

Ref	Expression
sylcom.1	⊢ (𝜑 → (𝜓 → 𝜒))
sylcom.2	⊢ (𝜓 → (𝜒 → 𝜃))

Assertion

Ref	Expression
sylcom	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylcom

Step	Hyp	Ref	Expression
1		sylcom.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylcom.2	. . 3 ⊢ (𝜓 → (𝜒 → 𝜃))
3	2	a2i 15	. 2 ⊢ ((𝜓 → 𝜒) → (𝜓 → 𝜃))
4	1, 3	syl 18	1 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl5com  32  syl6  36  syli  40  pm2.18d  128  mpbidi  244  2eu6  2682  dmcosseq  5960  dmcosseqOLD  5961  iss  6029  funopg  6566  funopsn  7143  limuni3  7852  frxp  8127  tz7.49  8439  dif1ennnALT  9252  frfi  9260  unblem3  9270  isfinite2  9274  iunfi  9316  tcrank  9882  setrec1lem2  9948  infdif  10267  isf34lem6  10439  axdc3lem4  10512  suplem1pr  11118  uzwo  13019  gsumcom2  20169  cmpsublem  23697  nrmhaus  24125  metrest  24823  finiunmbl  25845  h1datomi  32165  chirredlem1  32974  fnrelpredd  35699  r1omhfb  35717  r1omhfbregs  35778  mclsax  36303  antnestlaw2  36426  lineext  36811  in-ax8  36983  ss-ax8  36984  onsucconni  37195  dfttc4  37288  cbveud  38263  sdclem2  38644  heibor1lem  38711  iss2  39244  omabs2  44292  cotrintab  44573  tgblthelfgott  48857