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  2250  ax13ALT  2423  r19.30  3100  intss2  5072  vtoclr  5701  funopg  6550  feldmfvelcdm  7058  abnex  7733  xpider  8761  undifixp  8907  onsdominel  9090  fodomr  9092  fodomfir  9279  wemaplem2  9500  rankuni2b  9806  infxpenlem  9966  dfac8b  9984  ac10ct  9987  alephordi  10027  infdif  10161  cfflb  10212  alephval2  10525  tskxpss  10725  tskcard  10734  ingru  10768  grur1  10773  grothac  10783  suplem1pr  11005  mulgt0sr  11058  ixxssixx  13320  difelfzle  13602  swrdnd0  14622  climrlim2  15513  qshash  15793  gcdcllem3  16471  vdwlem13  16964  ocvsscon  21584  opsrtoslem2  21963  txcnp  23507  t0kq  23705  filconn  23770  filuni  23772  alexsubALTlem3  23936  rectbntr0  24721  iscau4  25179  cfilres  25196  lmcau  25213  bcthlem2  25225  onvf1odlem2  35091  subfacp1lem6  35172  cvmsdisj  35257  meran1  36399  bj-bi3ant  36577  bj-cbv3ta  36774  bj-2upleq  37000  bj-ismooredr2  37098  bj-snmoore  37101  bj-isclm  37279  relowlssretop  37351  poimirlem30  37644  poimirlem31  37645  caushft  37755  partimeq  38801  ax13fromc9  38899  harinf  43023  ntrk0kbimka  44028  onfrALTlem3  44534  onfrALTlem2  44536  e222  44626  e111  44664  e333  44722  bitr3VD  44838  disjinfi  45186  prpair  47502  onsetrec  49697  aacllem  49790