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  2251  ax13ALT  2424  r19.30  3097  intss2  5054  vtoclr  5677  funopg  6511  feldmfvelcdm  7014  abnex  7685  xpider  8707  undifixp  8853  onsdominel  9034  fodomr  9036  fodomfir  9207  wemaplem2  9428  rankuni2b  9738  infxpenlem  9896  dfac8b  9914  ac10ct  9917  alephordi  9957  infdif  10091  cfflb  10142  alephval2  10455  tskxpss  10655  tskcard  10664  ingru  10698  grur1  10703  grothac  10713  suplem1pr  10935  mulgt0sr  10988  ixxssixx  13251  difelfzle  13533  swrdnd0  14557  climrlim2  15446  qshash  15726  gcdcllem3  16404  vdwlem13  16897  ocvsscon  21605  opsrtoslem2  21984  txcnp  23528  t0kq  23726  filconn  23791  filuni  23793  alexsubALTlem3  23957  rectbntr0  24741  iscau4  25199  cfilres  25216  lmcau  25233  bcthlem2  25245  onvf1odlem2  35116  subfacp1lem6  35197  cvmsdisj  35282  meran1  36424  bj-bi3ant  36602  bj-cbv3ta  36799  bj-2upleq  37025  bj-ismooredr2  37123  bj-snmoore  37126  bj-isclm  37304  relowlssretop  37376  poimirlem30  37669  poimirlem31  37670  caushft  37780  partimeq  38826  ax13fromc9  38924  harinf  43046  ntrk0kbimka  44051  onfrALTlem3  44556  onfrALTlem2  44558  e222  44648  e111  44686  e333  44744  bitr3VD  44860  disjinfi  45208  prpair  47511  onsetrec  49719  aacllem  49812