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  2241  ax13ALT  2425  r19.30  3268  intss2  5037  vtoclr  5650  funopg  6468  abnex  7607  xpider  8577  undifixp  8722  onsdominel  8913  fodomr  8915  wemaplem2  9306  rankuni2b  9611  infxpenlem  9769  dfac8b  9787  ac10ct  9790  alephordi  9830  infdif  9965  cfflb  10015  alephval2  10328  tskxpss  10528  tskcard  10537  ingru  10571  grur1  10576  grothac  10586  suplem1pr  10808  mulgt0sr  10861  ixxssixx  13093  difelfzle  13369  swrdnd0  14370  climrlim2  15256  qshash  15539  gcdcllem3  16208  vdwlem13  16694  ocvsscon  20880  opsrtoslem2  21263  txcnp  22771  t0kq  22969  filconn  23034  filuni  23036  alexsubALTlem3  23200  rectbntr0  23995  iscau4  24443  cfilres  24460  lmcau  24477  bcthlem2  24489  subfacp1lem6  33147  cvmsdisj  33232  meran1  34600  bj-bi3ant  34771  bj-cbv3ta  34968  bj-2upleq  35202  bj-ismooredr2  35281  bj-snmoore  35284  bj-isclm  35462  relowlssretop  35534  poimirlem30  35807  poimirlem31  35808  caushft  35919  ax13fromc9  36920  harinf  40856  ntrk0kbimka  41649  onfrALTlem3  42164  onfrALTlem2  42166  e222  42256  e111  42294  e333  42353  bitr3VD  42469  disjinfi  42731  prpair  44953  onsetrec  46413  aacllem  46505