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

Theorem syl2im 38
 Description: Replace two antecedents. Implication-only version of syl2an 477. (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 32 . 2
51, 4syl 16 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4 This theorem is referenced by:  sylc  60  bi3antOLD  289  axc16g  1940  ax13  2047  axc16gOLD  2061  vtoclr  5049  funopg  5625  xpider  7401  undifixp  7525  onsdominel  7686  fodomr  7688  wemaplem2  7993  rankuni2b  8292  infxpenlem  8412  dfac8b  8433  ac10ct  8436  alephordi  8476  infdif  8610  cfflb  8660  alephval2  8968  tskxpss  9171  tskcard  9180  ingru  9214  grur1  9219  grothac  9229  suplem1pr  9451  mulgt0sr  9503  ixxssixx  11572  difelfzle  11817  climrlim2  13370  qshash  13639  gcdcllem3  14151  vdwlem13  14511  opsrtoslem2  18149  ocvsscon  18706  txcnp  20121  t0kq  20319  filcon  20384  filuni  20386  alexsubALTlem3  20549  rectbntr0  21337  iscau4  21718  cfilres  21735  lmcau  21751  bcthlem2  21764  3v3e3cycl1  24644  4cycl4v4e  24666  4cycl4dv4e  24668  clwlkfoclwwlk  24845  subfacp1lem6  28629  cvmsdisj  28715  meran1  29876  caushft  30254  harinf  30976  aacllem  33216  onfrALTlem3  33316  onfrALTlem2  33318  e222  33422  e111  33460  e333  33530  bitr3VD  33649  bj-bi3ant  34178  bj-cbv3ta  34270  bj-axc16g  34321  bj-2upleq  34570 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
 Copyright terms: Public domain W3C validator