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 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syl5com  32  syl6  36  syli  40  pm2.18d  128  mpbidi  244  2eu6  2686  dmcosseq  5959  dmcosseqOLD  5960  iss  6028  funopg  6559  funopsn  7134  limuni3  7836  frxp  8110  tz7.49  8420  dif1ennnALT  9225  frfi  9233  unblem3  9242  isfinite2  9246  iunfi  9288  tcrank  9844  infdif  10179  isf34lem6  10352  axdc3lem4  10425  suplem1pr  11025  uzwo  12926  gsumcom2  20036  cmpsublem  23517  nrmhaus  23944  metrest  24642  finiunmbl  25664  h1datomi  31842  chirredlem1  32651  fnrelpredd  35397  r1omhfb  35420  r1omhfbregs  35445  mclsax  35932  antnestlaw2  36055  lineext  36439  in-ax8  36597  ss-ax8  36598  onsucconni  36810  dfttc4  36903  cbveud  37878  sdclem2  38253  heibor1lem  38320  iss2  38855  omabs2  43921  cotrintab  44202  tgblthelfgott  48435  setrec1lem2  50317