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

Theorem necon3bbii 2686
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 2685 . 2  |-  ( A  =/=  B  <->  -.  ph )
43bicomi 206 1  |-  ( -. 
ph 
<->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 188    = wceq 1438    =/= wne 2619
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 2621
This theorem is referenced by:  necon1abii  2687  nssinpss  3706  difsnpss  4141  xpdifid  5282  wfi  5430  ordintdif  5489  tfi  6692  oelim2  7302  0sdomg  7705  fin23lem26  8757  axdc3lem4  8885  axdc4lem  8887  axcclem  8889  crreczi  12398  ef0lem  14126  lidlnz  18445  nconsubb  20430  ufileu  20926  itg2cnlem1  22711  plyeq0lem  23156  abelthlem2  23379  ppinprm  24071  chtnprm  24073  ltgov  24634  shne0i  27093  pjneli  27368  eleigvec  27602  nmo  28113  qqhval2lem  28787  qqhval2  28788  sibfof  29175  dffr5  30394  frind  30482  ellimits  30676  elicc3  30972  itg2addnclem2  31952  ftc1anclem3  31977  onfrALTlem5  36810  limcrecl  37573  usgra2pthlem1  39009
  Copyright terms: Public domain W3C validator