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 494. (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  2160  ax13ALT  2304  vtoclr  5162  funopg  5920  abnex  6962  xpider  7815  undifixp  7941  onsdominel  8106  fodomr  8108  wemaplem2  8449  rankuni2b  8713  infxpenlem  8833  dfac8b  8851  ac10ct  8854  alephordi  8894  infdif  9028  cfflb  9078  alephval2  9391  tskxpss  9591  tskcard  9600  ingru  9634  grur1  9639  grothac  9649  suplem1pr  9871  mulgt0sr  9923  ixxssixx  12186  difelfzle  12448  climrlim2  14272  qshash  14553  gcdcllem3  15217  vdwlem13  15691  opsrtoslem2  19479  ocvsscon  20013  txcnp  21417  t0kq  21615  filconn  21681  filuni  21683  alexsubALTlem3  21847  rectbntr0  22629  iscau4  23071  cfilres  23088  lmcau  23105  bcthlem2  23116  clwlksfoclwwlk  26956  subfacp1lem6  31152  cvmsdisj  31237  meran1  32394  bj-bi3ant  32558  bj-cbv3ta  32694  bj-2upleq  32984  bj-intss  33037  bj-snmoore  33052  relowlssretop  33191  poimirlem30  33419  poimirlem31  33420  caushft  33537  ax13fromc9  34017  harinf  37427  ntrk0kbimka  38163  onfrALTlem3  38585  onfrALTlem2  38587  e222  38687  e111  38725  e333  38786  bitr3VD  38910  onsetrec  42222  aacllem  42318
  Copyright terms: Public domain W3C validator