Theorem syl2im 40

Description: Replace two antecedents. Implication-only version of syl2an 589. (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  ax13ALT  2391  vtoclr  5414  funopg  6171  abnex  7245  xpider  8103  undifixp  8232  onsdominel  8399  fodomr  8401  wemaplem2  8743  rankuni2b  9015  infxpenlem  9171  dfac8b  9189  ac10ct  9192  alephordi  9232  infdif  9368  cfflb  9418  alephval2  9731  tskxpss  9931  tskcard  9940  ingru  9974  grur1  9979  grothac  9989  suplem1pr  10211  mulgt0sr  10264  ixxssixx  12505  difelfzle  12775  swrdnd0  13756  climrlim2  14690  qshash  14967  gcdcllem3  15633  vdwlem13  16105  opsrtoslem2  19885  ocvsscon  20422  txcnp  21836  t0kq  22034  filconn  22099  filuni  22101  alexsubALTlem3  22265  rectbntr0  23047  iscau4  23489  cfilres  23506  lmcau  23523  bcthlem2  23535  subfacp1lem6  31770  cvmsdisj  31855  meran1  32997  bj-bi3ant  33157  bj-cbv3ta  33302  bj-2upleq  33576  bj-intss  33630  bj-snmoore  33645  relowlssretop  33809  poimirlem30  34070  poimirlem31  34071  caushft  34186  ax13fromc9  35065  harinf  38570  ntrk0kbimka  39303  onfrALTlem3  39714  onfrALTlem2  39716  e222  39815  e111  39853  e333  39912  bitr3VD  40028  prpair  42450  onsetrec  43569  aacllem  43663