Theorem syl2im 40

Description: Replace two antecedents. Implication-only version of syl2an 597. (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  2241  ax13ALT  2424  r19.30  3120  intss2  5059  vtoclr  5685  funopg  6522  abnex  7673  xpider  8652  undifixp  8797  onsdominel  8995  fodomr  8997  wemaplem2  9408  rankuni2b  9714  infxpenlem  9874  dfac8b  9892  ac10ct  9895  alephordi  9935  infdif  10070  cfflb  10120  alephval2  10433  tskxpss  10633  tskcard  10642  ingru  10676  grur1  10681  grothac  10691  suplem1pr  10913  mulgt0sr  10966  ixxssixx  13198  difelfzle  13474  swrdnd0  14468  climrlim2  15355  qshash  15638  gcdcllem3  16307  vdwlem13  16791  ocvsscon  20985  opsrtoslem2  21368  txcnp  22876  t0kq  23074  filconn  23139  filuni  23141  alexsubALTlem3  23305  rectbntr0  24100  iscau4  24548  cfilres  24565  lmcau  24582  bcthlem2  24594  subfacp1lem6  33444  cvmsdisj  33529  meran1  34737  bj-bi3ant  34908  bj-cbv3ta  35105  bj-2upleq  35337  bj-ismooredr2  35435  bj-snmoore  35438  bj-isclm  35616  relowlssretop  35688  poimirlem30  35963  poimirlem31  35964  caushft  36075  partimeq  37127  ax13fromc9  37224  harinf  41170  ntrk0kbimka  42022  onfrALTlem3  42537  onfrALTlem2  42539  e222  42629  e111  42667  e333  42726  bitr3VD  42842  disjinfi  43110  prpair  45371  onsetrec  46831  aacllem  46923