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  2245  ax13ALT  2443  vtoclr  5610  funopg  6384  abnex  7473  xpider  8362  undifixp  8492  onsdominel  8660  fodomr  8662  wemaplem2  9005  rankuni2b  9276  infxpenlem  9433  dfac8b  9451  ac10ct  9454  alephordi  9494  infdif  9625  cfflb  9675  alephval2  9988  tskxpss  10188  tskcard  10197  ingru  10231  grur1  10236  grothac  10246  suplem1pr  10468  mulgt0sr  10521  ixxssixx  12746  difelfzle  13014  swrdnd0  14013  climrlim2  14898  qshash  15176  gcdcllem3  15844  vdwlem13  16323  opsrtoslem2  20259  ocvsscon  20813  txcnp  22222  t0kq  22420  filconn  22485  filuni  22487  alexsubALTlem3  22651  rectbntr0  23434  iscau4  23876  cfilres  23893  lmcau  23910  bcthlem2  23922  subfacp1lem6  32427  cvmsdisj  32512  meran1  33754  bj-bi3ant  33918  bj-cbv3ta  34103  bj-2upleq  34319  bj-intss  34385  bj-ismooredr2  34396  bj-snmoore  34399  bj-isclm  34566  relowlssretop  34638  poimirlem30  34916  poimirlem31  34917  caushft  35030  ax13fromc9  36036  harinf  39624  ntrk0kbimka  40382  onfrALTlem3  40871  onfrALTlem2  40873  e222  40963  e111  41001  e333  41060  bitr3VD  41176  prpair  43656  onsetrec  44803  aacllem  44895