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

Theorem necon3bbii 2639
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 202 . . 3  |-  ( A  =  B  <->  ph )
32necon3abii 2638 . 2  |-  ( A  =/=  B  <->  -.  ph )
43bicomi 202 1  |-  ( -. 
ph 
<->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    = wceq 1369    =/= wne 2606
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 185  df-ne 2608
This theorem is referenced by:  nssinpss  3582  difsnpss  4016  ordintdif  4768  xpdifid  5266  tfi  6464  oelim2  7034  0sdomg  7440  fin23lem26  8494  axdc3lem4  8622  axdc4lem  8624  axcclem  8626  crreczi  11989  ef0lem  13364  lidlnz  17310  nconsubb  19027  ufileu  19492  itg2cnlem1  21239  plyeq0lem  21678  abelthlem2  21897  ppinprm  22490  chtnprm  22492  shne0i  24851  pjneli  25126  eleigvec  25361  nmo  25869  qqhval2lem  26410  qqhval2  26411  sibfof  26726  dffr5  27563  wfi  27668  frind  27704  ellimits  27941  itg2addnclem2  28444  ftc1anclem3  28469  elicc3  28512  usgra2pthlem1  30300  onfrALTlem5  31250
  Copyright terms: Public domain W3C validator