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  2244  ax13ALT  2425  r19.30  3265  intss2  5033  vtoclr  5641  funopg  6452  abnex  7585  xpider  8535  undifixp  8680  onsdominel  8862  fodomr  8864  wemaplem2  9236  rankuni2b  9542  infxpenlem  9700  dfac8b  9718  ac10ct  9721  alephordi  9761  infdif  9896  cfflb  9946  alephval2  10259  tskxpss  10459  tskcard  10468  ingru  10502  grur1  10507  grothac  10517  suplem1pr  10739  mulgt0sr  10792  ixxssixx  13022  difelfzle  13298  swrdnd0  14298  climrlim2  15184  qshash  15467  gcdcllem3  16136  vdwlem13  16622  ocvsscon  20792  opsrtoslem2  21173  txcnp  22679  t0kq  22877  filconn  22942  filuni  22944  alexsubALTlem3  23108  rectbntr0  23901  iscau4  24348  cfilres  24365  lmcau  24382  bcthlem2  24394  subfacp1lem6  33047  cvmsdisj  33132  meran1  34527  bj-bi3ant  34698  bj-cbv3ta  34895  bj-2upleq  35129  bj-ismooredr2  35208  bj-snmoore  35211  bj-isclm  35389  relowlssretop  35461  poimirlem30  35734  poimirlem31  35735  caushft  35846  ax13fromc9  36847  harinf  40772  ntrk0kbimka  41538  onfrALTlem3  42053  onfrALTlem2  42055  e222  42145  e111  42183  e333  42242  bitr3VD  42358  disjinfi  42620  prpair  44841  onsetrec  46299  aacllem  46391