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  34  syli  38  mpbidi  230  2eu6  2546  dmcosseq  5308  iss  5367  funopg  5836  limuni3  6944  frxp  7174  wfrlem12  7313  tz7.49  7427  dif1en  8078  enp1i  8080  frfi  8090  unblem3  8099  isfinite2  8103  iunfi  8137  tcrank  8630  infdif  8914  isf34lem6  9085  axdc3lem4  9158  suplem1pr  9753  uzwo  11627  gsumcom2  18197  cmpsublem  21012  nrmhaus  21439  metrest  22139  finiunmbl  23119  wilthlem3  24596  cusgrafi  26010  clwwlkn0  26302  h1datomi  27824  chirredlem1  28633  mclsax  30720  frrlem11  31036  lineext  31353  onsucconi  31606  sdclem2  32708  heibor1lem  32778  cotrintab  36940  tgblthelfgott  40229  tgblthelfgottOLD  40236  setrec1lem2  42234