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

Theorem pm2.61dne 2675
Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
pm2.61dne.1  |-  ( ph  ->  ( A  =  B  ->  ps ) )
pm2.61dne.2  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )
Assertion
Ref Expression
pm2.61dne  |-  ( ph  ->  ps )

Proof of Theorem pm2.61dne
StepHypRef Expression
1 pm2.61dne.2 . 2  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )
2 nne 2602 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
3 pm2.61dne.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  ps ) )
42, 3syl5bi 209 . 2  |-  ( ph  ->  ( -.  A  =/= 
B  ->  ps )
)
51, 4pm2.61d 152 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1652    =/= wne 2598
This theorem is referenced by:  pm2.61dane  2676  wefrc  4568  wereu2  4571  oe0lem  6749  fisupg  7347  marypha1lem  7430  wdomtr  7535  unxpwdom2  7548  fpwwe2lem13  8509  grur1a  8686  grutsk  8689  fimaxre2  9948  xlesubadd  10834  sqreu  12156  pcxcl  13226  pcmpt  13253  isabvd  15900  lspprat  16217  ordtrest2lem  17259  ordthauslem  17439  fbssint  17862  fclscf  18049  tgptsmscld  18172  ovoliunnul  19395  itg11  19575  i1fadd  19579  fta1g  20082  plydiveu  20207  fta1  20217  mulcxp  20568  cxpsqr  20586  ostth3  21324  subfacp1lem5  24862  frmin  25509  brbtwn2  25836  colinearalg  25841  btwnexch2  25949  limsucncmpi  26187  areacirc  26288  comppfsc  26378  fnemeet2  26387  fnejoin2  26389  sstotbnd2  26474  ssbnd  26488  prdsbnd2  26495  rrncmslem  26532  symggen  27379  atnlt  30048  atlelt  30172  llnnlt  30257  lplnnlt  30299  lvolnltN  30352  pmapglb2N  30505  pmapglb2xN  30506  paddasslem14  30567  cdleme27a  31101
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 178  df-ne 2600
  Copyright terms: Public domain W3C validator