Theorem syl2im 40

Description: Replace two antecedents. Implication-only version of syl2an 596. (Contributed by Wolf Lammen, 14-May-2013.)

Hypotheses

Ref	Expression
syl2im.1	⊢ (𝜑 → 𝜓)
syl2im.2	⊢ (𝜒 → 𝜃)
syl2im.3	⊢ (𝜓 → (𝜃 → 𝜏))

Assertion

Ref	Expression
syl2im	⊢ (𝜑 → (𝜒 → 𝜏))

Proof of Theorem syl2im

Step	Hyp	Ref	Expression
1		syl2im.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl2im.2	. . 3 ⊢ (𝜒 → 𝜃)
3		syl2im.3	. . 3 ⊢ (𝜓 → (𝜃 → 𝜏))
4	2, 3	syl5 34	. 2 ⊢ (𝜓 → (𝜒 → 𝜏))
5	1, 4	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:  syl2imc  41  sylc  65  sbequ2  2249  ax13ALT  2430  r19.30  3120  intss2  5108  vtoclr  5748  funopg  6600  feldmfvelcdm  7106  abnex  7777  xpider  8828  undifixp  8974  onsdominel  9166  fodomr  9168  fodomfir  9368  wemaplem2  9587  rankuni2b  9893  infxpenlem  10053  dfac8b  10071  ac10ct  10074  alephordi  10114  infdif  10248  cfflb  10299  alephval2  10612  tskxpss  10812  tskcard  10821  ingru  10855  grur1  10860  grothac  10870  suplem1pr  11092  mulgt0sr  11145  ixxssixx  13401  difelfzle  13681  swrdnd0  14695  climrlim2  15583  qshash  15863  gcdcllem3  16538  vdwlem13  17031  ocvsscon  21693  opsrtoslem2  22080  txcnp  23628  t0kq  23826  filconn  23891  filuni  23893  alexsubALTlem3  24057  rectbntr0  24854  iscau4  25313  cfilres  25330  lmcau  25347  bcthlem2  25359  subfacp1lem6  35190  cvmsdisj  35275  meran1  36412  bj-bi3ant  36590  bj-cbv3ta  36787  bj-2upleq  37013  bj-ismooredr2  37111  bj-snmoore  37114  bj-isclm  37292  relowlssretop  37364  poimirlem30  37657  poimirlem31  37658  caushft  37768  partimeq  38810  ax13fromc9  38907  harinf  43046  ntrk0kbimka  44052  onfrALTlem3  44564  onfrALTlem2  44566  e222  44656  e111  44694  e333  44753  bitr3VD  44869  disjinfi  45197  prpair  47488  onsetrec  49227  aacllem  49320