Theorem sylcom 30

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 14	. 2 ⊢ ((𝜓 → 𝜒) → (𝜓 → 𝜃))
4	1, 3	syl 17	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  31  syl6  35  syli  39  pm2.18d  127  mpbidi  243  2eu6  2682  dmcosseq  5952  dmcosseqOLD  5953  dmcosseqOLDOLD  5954  iss  6021  funopg  6551  funopsn  7126  limuni3  7828  frxp  8101  tz7.49  8411  dif1ennnALT  9217  frfi  9225  unblem3  9234  isfinite2  9238  iunfi  9283  tcrank  9839  infdif  10161  isf34lem6  10334  axdc3lem4  10407  suplem1pr  11007  uzwo  12909  gsumcom2  19998  cmpsublem  23439  nrmhaus  23866  metrest  24564  finiunmbl  25586  h1datomi  31730  chirredlem1  32539  fnrelpredd  35351  r1omhfb  35372  r1omhfbregs  35397  mclsax  35883  antnestlaw2  36006  lineext  36390  in-ax8  36548  ss-ax8  36549  onsucconni  36761  dfttc4  36854  cbveud  37830  sdclem2  38205  heibor1lem  38272  iss2  38807  omabs2  43873  cotrintab  44154  tgblthelfgott  48401  setrec1lem2  50273