Theorem syl2im 40

Description: Replace two antecedents. Implication-only version of syl2an 595. (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  2233  ax13ALT  2416  r19.30  3112  intss2  5102  vtoclr  5730  funopg  6573  abnex  7738  xpider  8779  undifixp  8925  onsdominel  9123  fodomr  9125  wemaplem2  9539  rankuni2b  9845  infxpenlem  10005  dfac8b  10023  ac10ct  10026  alephordi  10066  infdif  10201  cfflb  10251  alephval2  10564  tskxpss  10764  tskcard  10773  ingru  10807  grur1  10812  grothac  10822  suplem1pr  11044  mulgt0sr  11097  ixxssixx  13336  difelfzle  13612  swrdnd0  14605  climrlim2  15489  qshash  15771  gcdcllem3  16441  vdwlem13  16927  ocvsscon  21538  opsrtoslem2  21929  txcnp  23448  t0kq  23646  filconn  23711  filuni  23713  alexsubALTlem3  23877  rectbntr0  24672  iscau4  25131  cfilres  25148  lmcau  25165  bcthlem2  25177  subfacp1lem6  34667  cvmsdisj  34752  meran1  35787  bj-bi3ant  35958  bj-cbv3ta  36155  bj-2upleq  36384  bj-ismooredr2  36482  bj-snmoore  36485  bj-isclm  36663  relowlssretop  36735  poimirlem30  37012  poimirlem31  37013  caushft  37123  partimeq  38173  ax13fromc9  38270  harinf  42287  ntrk0kbimka  43304  onfrALTlem3  43819  onfrALTlem2  43821  e222  43911  e111  43949  e333  44008  bitr3VD  44124  disjinfi  44401  prpair  46679  onsetrec  47965  aacllem  48060