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

Theorem pm2.61ine 2605
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  |-  ( A  =  B  ->  ph )
pm2.61ine.2  |-  ( A  =/=  B  ->  ph )
Assertion
Ref Expression
pm2.61ine  |-  ph

Proof of Theorem pm2.61ine
StepHypRef Expression
1 pm2.61ine.2 . 2  |-  ( A  =/=  B  ->  ph )
2 nne 2533 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
3 pm2.61ine.1 . . 3  |-  ( A  =  B  ->  ph )
42, 3sylbi 187 . 2  |-  ( -.  A  =/=  B  ->  ph )
51, 4pm2.61i 156 1  |-  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1647    =/= wne 2529
This theorem is referenced by:  rgenz  3648  raaan  3650  raaanv  3651  iinrab2  4067  riinrab  4079  reusv2lem2  4639  reusv6OLD  4648  reusv7OLD  4649  xpriindi  4925  dmxpid  5001  dmxpss  5210  rnxpid  5212  xpexr  5217  cnvpo  5316  fconstfv  5854  frxp  6353  fodomr  7155  wdompwdom  7439  inf3lemd  7475  en3lp  7565  prdom2  7783  iunfictbso  7888  infpssrlem4  8079  1re  8984  00id  9134  ioorebas  10898  fzfi  11198  hash2prde  11575  cntzssv  15014  plyssc  19797  usgra2edg  21079  siii  21865  h1de2ctlem  22568  riesz3i  23076  unierri  23118  dedekindle  24757  dfpo2  24938  axsegcon  25382  axpaschlem  25395  axlowdimlem16  25412  axcontlem7  25425  axcontlem8  25426  axcontlem12  25430  cgrextend  25458  ifscgr  25494  idinside  25534  btwnconn1lem12  25548  btwnconn1  25551  linethru  25603  ovoliunnfl  25756  voliunnfl  25758  volsupnfl  25759  psgnunilem4  27011  sdrgacs  27100  usgrcyclnl2  27776  4cycl4dv  27802  1to3vfriswmgra  27831  a9e2ndeq  28060  bnj1143  28574  bnj571  28690  bnj594  28696  bnj852  28705
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-ne 2531
  Copyright terms: Public domain W3C validator