MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2im Structured version   Visualization version   GIF version

Theorem syl2im 40
Description: Replace two antecedents. Implication-only version of syl2an 585. (Contributed by Wolf Lammen, 14-May-2013.)
Hypotheses
Ref Expression
syl2im.1 (𝜑𝜓)
syl2im.2 (𝜒𝜃)
syl2im.3 (𝜓 → (𝜃𝜏))
Assertion
Ref Expression
syl2im (𝜑 → (𝜒𝜏))

Proof of Theorem syl2im
StepHypRef Expression
1 syl2im.1 . 2 (𝜑𝜓)
2 syl2im.2 . . 3 (𝜒𝜃)
3 syl2im.3 . . 3 (𝜓 → (𝜃𝜏))
42, 3syl5 34 . 2 (𝜓 → (𝜒𝜏))
51, 4syl 17 1 (𝜑 → (𝜒𝜏))
Colors of variables: wff setvar class
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  axc16gOLD  2336  ax13ALT  2473  vtoclr  5362  funopg  6133  abnex  7193  xpider  8051  undifixp  8179  onsdominel  8346  fodomr  8348  wemaplem2  8689  rankuni2b  8961  infxpenlem  9117  dfac8b  9135  ac10ct  9138  alephordi  9178  infdif  9314  cfflb  9364  alephval2  9677  tskxpss  9877  tskcard  9886  ingru  9920  grur1  9925  grothac  9935  suplem1pr  10157  mulgt0sr  10209  ixxssixx  12405  difelfzle  12674  climrlim2  14499  qshash  14779  gcdcllem3  15440  vdwlem13  15912  opsrtoslem2  19691  ocvsscon  20227  txcnp  21635  t0kq  21833  filconn  21898  filuni  21900  alexsubALTlem3  22064  rectbntr0  22846  iscau4  23287  cfilres  23304  lmcau  23321  bcthlem2  23332  clwlksfoclwwlkOLD  27235  subfacp1lem6  31488  cvmsdisj  31573  meran1  32725  bj-bi3ant  32887  bj-cbv3ta  33023  bj-2upleq  33308  bj-intss  33362  bj-snmoore  33377  relowlssretop  33525  poimirlem30  33750  poimirlem31  33751  caushft  33866  ax13fromc9  34683  harinf  38100  ntrk0kbimka  38835  onfrALTlem3  39255  onfrALTlem2  39257  e222  39357  e111  39395  e333  39455  bitr3VD  39576  onsetrec  43020  aacllem  43116
  Copyright terms: Public domain W3C validator