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

Theorem syl2im 39
Description: Replace two antecedents. Implication-only version of syl2an 492. (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 33 . 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:  sylc  62  axc16gOLD  2145  ax13OLD  2292  vtoclr  5076  funopg  5822  xpider  7682  undifixp  7807  onsdominel  7971  fodomr  7973  wemaplem2  8312  rankuni2b  8576  infxpenlem  8696  dfac8b  8714  ac10ct  8717  alephordi  8757  infdif  8891  cfflb  8941  alephval2  9250  tskxpss  9450  tskcard  9459  ingru  9493  grur1  9498  grothac  9508  suplem1pr  9730  mulgt0sr  9782  ixxssixx  12016  difelfzle  12276  climrlim2  14072  qshash  14344  gcdcllem3  15007  vdwlem13  15481  opsrtoslem2  19252  ocvsscon  19780  txcnp  21175  t0kq  21373  filcon  21439  filuni  21441  alexsubALTlem3  21605  rectbntr0  22375  iscau4  22803  cfilres  22820  lmcau  22836  bcthlem2  22847  3v3e3cycl1  25938  4cycl4v4e  25960  4cycl4dv4e  25962  clwlkfoclwwlk  26138  subfacp1lem6  30227  cvmsdisj  30312  meran1  31386  bj-bi3ant  31553  bj-cbv3ta  31703  bj-2upleq  31996  relowlssretop  32190  poimirlem30  32412  poimirlem31  32413  caushft  32530  ax13fromc9  33012  harinf  36422  ntrk0kbimka  37160  onfrALTlem3  37583  onfrALTlem2  37585  e222  37685  e111  37723  e333  37784  bitr3VD  37909  clwlksfoclwwlk  41272  aacllem  42319
  Copyright terms: Public domain W3C validator