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

Theorem pm2.61ine 3026
Description: Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
pm2.61ine.1 (𝐴 = 𝐵𝜑)
pm2.61ine.2 (𝐴𝐵𝜑)
Assertion
Ref Expression
pm2.61ine 𝜑

Proof of Theorem pm2.61ine
StepHypRef Expression
1 pm2.61ine.2 . 2 (𝐴𝐵𝜑)
2 nne 2945 . . 3 𝐴𝐵𝐴 = 𝐵)
3 pm2.61ine.1 . . 3 (𝐴 = 𝐵𝜑)
42, 3sylbi 220 . 2 𝐴𝐵𝜑)
51, 4pm2.61i 185 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1543  wne 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 210  df-ne 2942
This theorem is referenced by:  pm2.61ne  3028  pm2.61dne  3029  pm2.61iine  3033  raaan  4447  raaanv  4448  iinrab2  4993  iinvdif  5003  riinrab  5007  reusv2lem2  5307  po2ne  5499  xpriindi  5720  dmxpid  5814  dmxpss  6049  rnxpid  6051  cnvpo  6165  xpcoid  6168  dfpo2  6174  fnprb  7043  fntpb  7044  xpexr  7715  frxp  7914  suppimacnv  7937  fodomr  8820  wdompwdom  9219  en3lp  9254  inf3lemd  9267  prdom2  9645  iunfictbso  9753  infpssrlem4  9945  1re  10858  dedekindle  11021  00id  11032  nn0lt2  12265  nn01to3  12562  ioorebas  13064  fzfi  13572  ssnn0fi  13585  hash2prde  14064  repswsymballbi  14373  cshw0  14387  cshwmodn  14388  cshwsublen  14389  cshwn  14390  cshwlen  14392  cshwidx0  14399  dmtrclfv  14609  cncongr2  16253  cshwsidrepswmod0  16676  cshwshashlem1  16677  cshwshashlem2  16678  cshwsdisj  16680  cntzssv  18750  psgnunilem4  18917  sdrgacs  19873  mulmarep1gsum2  21498  plyssc  25121  cxpsqrtth  25644  addsqnreup  26351  2sqreultlem  26355  2sqreunnltlem  26358  axsegcon  27045  axpaschlem  27058  axlowdimlem16  27075  axcontlem7  27088  axcontlem8  27089  axcontlem12  27093  umgrislfupgrlem  27240  edglnl  27261  uhgr2edg  27323  1egrvtxdg0  27626  uspgrn2crct  27919  2pthon3v  28054  clwwlknon0  28203  1pthon2v  28263  1to3vfriswmgr  28390  frgrnbnb  28403  numclwwlk5  28498  siii  28961  h1de2ctlem  29663  riesz3i  30170  unierri  30212  dya2iocuni  31989  sibf0  32040  bnj1143  32509  bnj571  32625  bnj594  32631  bnj852  32640  noresle  33666  cgrextend  34076  ifscgr  34112  idinside  34152  btwnconn1lem12  34166  btwnconn1  34169  linethru  34221  bj-xpnzex  34915  ovoliunnfl  35586  voliunnfl  35588  volsupnfl  35589  sn-1ne2  40036  ax6e2ndeq  41885  lighneal  44767  nrhmzr  45135  zlmodzxznm  45542  itsclc0yqe  45811
  Copyright terms: Public domain W3C validator