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

Theorem necon3bbii 2673
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 206 . . 3  |-  ( A  =  B  <->  ph )
32necon3abii 2672 . 2  |-  ( A  =/=  B  <->  -.  ph )
43bicomi 206 1  |-  ( -. 
ph 
<->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 188    = wceq 1446    =/= wne 2624
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 189  df-ne 2626
This theorem is referenced by:  necon1abii  2674  nssinpss  3677  difsnpss  4118  xpdifid  5268  wfi  5416  ordintdif  5475  tfi  6685  oelim2  7301  0sdomg  7706  fin23lem26  8760  axdc3lem4  8888  axdc4lem  8890  axcclem  8892  crreczi  12404  ef0lem  14145  lidlnz  18464  nconsubb  20450  ufileu  20946  itg2cnlem1  22731  plyeq0lem  23176  abelthlem2  23399  ppinprm  24091  chtnprm  24093  ltgov  24654  shne0i  27113  pjneli  27388  eleigvec  27622  nmo  28133  qqhval2lem  28797  qqhval2  28798  sibfof  29185  dffr5  30405  frind  30493  ellimits  30689  elicc3  30985  itg2addnclem2  32006  ftc1anclem3  32031  onfrALTlem5  36919  limcrecl  37719  usgra2pthlem1  39771
  Copyright terms: Public domain W3C validator