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

Theorem necon3bbii 2728
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 2727 . 2  |-  ( A  =/=  B  <->  -.  ph )
43bicomi 202 1  |-  ( -. 
ph 
<->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    = wceq 1379    =/= wne 2662
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 2664
This theorem is referenced by:  necon1abii  2729  nssinpss  3730  difsnpss  4170  ordintdif  4927  xpdifid  5435  tfi  6672  oelim2  7244  0sdomg  7646  fin23lem26  8705  axdc3lem4  8833  axdc4lem  8835  axcclem  8837  crreczi  12259  ef0lem  13676  lidlnz  17675  nconsubb  19718  ufileu  20183  itg2cnlem1  21931  plyeq0lem  22370  abelthlem2  22589  ppinprm  23182  chtnprm  23184  shne0i  26070  pjneli  26345  eleigvec  26580  nmo  27088  qqhval2lem  27626  qqhval2  27627  sibfof  27950  dffr5  28787  wfi  28892  frind  28928  ellimits  29165  itg2addnclem2  29672  ftc1anclem3  29697  elicc3  29740  limcrecl  31199  usgra2pthlem1  31848  onfrALTlem5  32412
  Copyright terms: Public domain W3C validator