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  2684  dmcosseq  5970  dmcosseqOLD  5971  iss  6039  funopg  6572  funopsn  7146  limuni3  7849  frxp  8123  tz7.49  8433  dif1ennnALT  9238  frfi  9246  unblem3  9255  isfinite2  9259  iunfi  9301  tcrank  9857  infdif  10192  isf34lem6  10365  axdc3lem4  10438  suplem1pr  11038  uzwo  12936  gsumcom2  20046  cmpsublem  23537  nrmhaus  23964  metrest  24662  finiunmbl  25684  h1datomi  31911  chirredlem1  32720  fnrelpredd  35460  r1omhfb  35486  r1omhfbregs  35528  mclsax  36039  antnestlaw2  36162  lineext  36546  in-ax8  36714  ss-ax8  36715  onsucconni  36926  dfttc4  37019  cbveud  37996  sdclem2  38371  heibor1lem  38438  iss2  38971  omabs2  44039  cotrintab  44320  tgblthelfgott  48557  setrec1lem2  50443