Theorem syl2im 40

Description: Replace two antecedents. Implication-only version of syl2an 597. (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  2257  ax13ALT  2430  r19.30  3104  intss2  5064  vtoclr  5688  funopg  6527  feldmfvelcdm  7033  abnex  7705  xpider  8730  undifixp  8877  onsdominel  9059  fodomr  9061  fodomfir  9233  wemaplem2  9457  rankuni2b  9770  infxpenlem  9928  dfac8b  9946  ac10ct  9949  alephordi  9989  infdif  10123  cfflb  10174  alephval2  10488  tskxpss  10688  tskcard  10697  ingru  10731  grur1  10736  grothac  10746  suplem1pr  10968  mulgt0sr  11021  ixxssixx  13280  difelfzle  13562  swrdnd0  14586  climrlim2  15475  qshash  15755  gcdcllem3  16433  vdwlem13  16926  ocvsscon  21635  opsrtoslem2  22016  txcnp  23569  t0kq  23767  filconn  23832  filuni  23834  alexsubALTlem3  23998  rectbntr0  24782  iscau4  25240  cfilres  25257  lmcau  25274  bcthlem2  25286  onvf1odlem2  35311  subfacp1lem6  35392  cvmsdisj  35477  meran1  36618  bj-bi3ant  36802  bj-cbv3ta  37000  bj-2upleq  37226  bj-ismooredr2  37328  bj-snmoore  37331  bj-isclm  37509  relowlssretop  37581  poimirlem30  37864  poimirlem31  37865  caushft  37975  partimeq  39126  ax13fromc9  39245  harinf  43354  ntrk0kbimka  44358  onfrALTlem3  44863  onfrALTlem2  44865  e222  44955  e111  44993  e333  45051  bitr3VD  45167  disjinfi  45514  prpair  47824  onsetrec  50030  aacllem  50123