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

Theorem necon3bbii 2490
Description: Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
Hypothesis
Ref Expression
necon3bbii.1  |-  ( ph  <->  A  =  B )
Assertion
Ref Expression
necon3bbii  |-  ( -. 
ph 
<->  A  =/=  B )

Proof of Theorem necon3bbii
StepHypRef Expression
1 necon3bbii.1 . . . 4  |-  ( ph  <->  A  =  B )
21bicomi 193 . . 3  |-  ( A  =  B  <->  ph )
32necon3abii 2489 . 2  |-  ( A  =/=  B  <->  -.  ph )
43bicomi 193 1  |-  ( -. 
ph 
<->  A  =/=  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    = wceq 1632    =/= wne 2459
This theorem is referenced by:  nssinpss  3414  difsnpss  3774  ordintdif  4457  tfi  4660  oelim2  6609  0sdomg  7006  fin23lem26  7967  axdc3lem4  8095  axdc4lem  8097  axcclem  8099  crreczi  11242  ef0lem  12376  lidlnz  15996  nconsubb  17165  ufileu  17630  itg2cnlem1  19132  plyeq0lem  19608  abelthlem2  19824  isosctrlem1  20134  ppinprm  20406  chtnprm  20408  shne0i  22043  pjneli  22318  eleigvec  22553  nmo  23160  dffr5  24181  wfi  24278  frind  24314  ellimits  24521  itg2addnclem2  25004  nbssntrs  26250  elicc3  26331  onfrALTlem5  28606
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 2461
  Copyright terms: Public domain W3C validator