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

Theorem necon3bbii 2664
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 2663 . 2  |-  ( A  =/=  B  <->  -.  ph )
43bicomi 202 1  |-  ( -. 
ph 
<->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    = wceq 1405    =/= wne 2598
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 2600
This theorem is referenced by:  necon1abii  2665  nssinpss  3681  difsnpss  4114  xpdifid  5252  wfi  5399  ordintdif  5458  tfi  6670  oelim2  7280  0sdomg  7683  fin23lem26  8736  axdc3lem4  8864  axdc4lem  8866  axcclem  8868  crreczi  12333  ef0lem  14021  lidlnz  18194  nconsubb  20214  ufileu  20710  itg2cnlem1  22458  plyeq0lem  22897  abelthlem2  23117  ppinprm  23805  chtnprm  23807  ltgov  24365  shne0i  26766  pjneli  27041  eleigvec  27275  nmo  27785  qqhval2lem  28400  qqhval2  28401  sibfof  28774  dffr5  29953  frind  30041  ellimits  30235  elicc3  30532  itg2addnclem2  31420  ftc1anclem3  31445  onfrALTlem5  36318  limcrecl  36984  usgra2pthlem1  37963
  Copyright terms: Public domain W3C validator