Theorem syl2im 40

Description: Replace two antecedents. Implication-only version of syl2an 494. (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  axc16gOLD  2161  ax13ALT  2305  vtoclr  5164  funopg  5922  abnex  6965  xpider  7818  undifixp  7944  onsdominel  8109  fodomr  8111  wemaplem2  8452  rankuni2b  8716  infxpenlem  8836  dfac8b  8854  ac10ct  8857  alephordi  8897  infdif  9031  cfflb  9081  alephval2  9394  tskxpss  9594  tskcard  9603  ingru  9637  grur1  9642  grothac  9652  suplem1pr  9874  mulgt0sr  9926  ixxssixx  12189  difelfzle  12452  climrlim2  14278  qshash  14559  gcdcllem3  15223  vdwlem13  15697  opsrtoslem2  19485  ocvsscon  20019  txcnp  21423  t0kq  21621  filconn  21687  filuni  21689  alexsubALTlem3  21853  rectbntr0  22635  iscau4  23077  cfilres  23094  lmcau  23111  bcthlem2  23122  clwlksfoclwwlk  26963  subfacp1lem6  31167  cvmsdisj  31252  meran1  32410  bj-bi3ant  32574  bj-cbv3ta  32710  bj-2upleq  33000  bj-intss  33053  bj-snmoore  33068  relowlssretop  33211  poimirlem30  33439  poimirlem31  33440  caushft  33557  ax13fromc9  34191  harinf  37601  ntrk0kbimka  38337  onfrALTlem3  38759  onfrALTlem2  38761  e222  38861  e111  38899  e333  38960  bitr3VD  39084  onsetrec  42451  aacllem  42547