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  2237  ax13ALT  2420  r19.30  3116  intss2  5105  vtoclr  5735  funopg  6581  feldmfvelcdm  7090  abnex  7753  xpider  8800  undifixp  8946  onsdominel  9144  fodomr  9146  wemaplem2  9564  rankuni2b  9870  infxpenlem  10030  dfac8b  10048  ac10ct  10051  alephordi  10091  infdif  10226  cfflb  10276  alephval2  10589  tskxpss  10789  tskcard  10798  ingru  10832  grur1  10837  grothac  10847  suplem1pr  11069  mulgt0sr  11122  ixxssixx  13364  difelfzle  13640  swrdnd0  14633  climrlim2  15517  qshash  15799  gcdcllem3  16469  vdwlem13  16955  ocvsscon  21600  opsrtoslem2  21993  txcnp  23517  t0kq  23715  filconn  23780  filuni  23782  alexsubALTlem3  23946  rectbntr0  24741  iscau4  25200  cfilres  25217  lmcau  25234  bcthlem2  25246  subfacp1lem6  34789  cvmsdisj  34874  meran1  35889  bj-bi3ant  36060  bj-cbv3ta  36257  bj-2upleq  36485  bj-ismooredr2  36583  bj-snmoore  36586  bj-isclm  36764  relowlssretop  36836  poimirlem30  37117  poimirlem31  37118  caushft  37228  partimeq  38275  ax13fromc9  38372  harinf  42449  ntrk0kbimka  43463  onfrALTlem3  43977  onfrALTlem2  43979  e222  44069  e111  44107  e333  44166  bitr3VD  44282  disjinfi  44559  prpair  46835  onsetrec  48133  aacllem  48228