Theorem syl2im 40

Description: Replace two antecedents. Implication-only version of syl2an 605. (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  sbi1lem  2103  sbequ2  2285  ax13ALT  2457  r19.30  3130  intss2  5066  vtoclr  5711  funopg  6555  feldmfvelcdm  7067  abnex  7740  xpider  8770  undifixp  8916  onsdominel  9098  fodomr  9100  fodomfir  9271  wemaplem2  9493  rankuni2b  9809  infxpenlem  9981  dfac8b  9999  ac10ct  10002  alephordi  10042  infdif  10175  cfflb  10227  alephval2  10541  tskxpss  10741  tskcard  10750  ingru  10784  grur1  10789  grothac  10799  suplem1pr  11021  mulgt0sr  11074  ixxssixx  13373  difelfzle  13656  swrdnd0  14681  climrlim2  15584  qshash  15865  gcdcllem3  16545  vdwlem13  17039  ocvsscon  21734  opsrtoslem2  22116  txcnp  23687  t0kq  23885  filconn  23950  filuni  23952  alexsubALTlem3  24116  rectbntr0  24900  iscau4  25348  cfilres  25365  lmcau  25382  bcthlem2  25394  onvf1odlem2  35451  subfacp1lem6  35540  cvmsdisj  35625  meran1  36776  bj-bi3ant  37037  bj-cbv3ta  37276  bj-2upleq  37502  bj-ismooredr2  37605  bj-snmoore  37608  bj-isclm  37788  relowlssretop  37862  poimirlem30  38154  poimirlem31  38155  caushft  38265  partimeq  39416  ax13fromc9  39535  harinf  43616  ntrk0kbimka  44620  onfrALTlem3  45111  onfrALTlem2  45113  e222  45203  e111  45241  e333  45299  bitr3VD  45415  disjinfi  45761  prpair  48098  onsetrec  50320  aacllem  50413