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  2250  ax13ALT  2433  r19.30  3126  intss2  5131  vtoclr  5763  funopg  6612  feldmfvelcdm  7120  abnex  7792  xpider  8846  undifixp  8992  onsdominel  9192  fodomr  9194  fodomfir  9396  wemaplem2  9616  rankuni2b  9922  infxpenlem  10082  dfac8b  10100  ac10ct  10103  alephordi  10143  infdif  10277  cfflb  10328  alephval2  10641  tskxpss  10841  tskcard  10850  ingru  10884  grur1  10889  grothac  10899  suplem1pr  11121  mulgt0sr  11174  ixxssixx  13421  difelfzle  13698  swrdnd0  14705  climrlim2  15593  qshash  15875  gcdcllem3  16547  vdwlem13  17040  ocvsscon  21716  opsrtoslem2  22103  txcnp  23649  t0kq  23847  filconn  23912  filuni  23914  alexsubALTlem3  24078  rectbntr0  24873  iscau4  25332  cfilres  25349  lmcau  25366  bcthlem2  25378  subfacp1lem6  35153  cvmsdisj  35238  meran1  36377  bj-bi3ant  36555  bj-cbv3ta  36752  bj-2upleq  36978  bj-ismooredr2  37076  bj-snmoore  37079  bj-isclm  37257  relowlssretop  37329  poimirlem30  37610  poimirlem31  37611  caushft  37721  partimeq  38765  ax13fromc9  38862  harinf  42991  ntrk0kbimka  44001  onfrALTlem3  44515  onfrALTlem2  44517  e222  44607  e111  44645  e333  44704  bitr3VD  44820  disjinfi  45099  prpair  47375  onsetrec  48800  aacllem  48895