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

Theorem necon3bbii 2634
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 195 . . 3  |-  ( A  =  B  <->  ph )
32necon3abii 2633 . 2  |-  ( A  =/=  B  <->  -.  ph )
43bicomi 195 1  |-  ( -. 
ph 
<->  A  =/=  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 178    = wceq 1653    =/= wne 2601
This theorem is referenced by:  nssinpss  3575  difsnpss  3943  ordintdif  4632  tfi  4835  oelim2  6840  0sdomg  7238  fin23lem26  8207  axdc3lem4  8335  axdc4lem  8337  axcclem  8339  crreczi  11506  ef0lem  12683  lidlnz  16301  nconsubb  17488  ufileu  17953  itg2cnlem1  19655  plyeq0lem  20131  abelthlem2  20350  ppinprm  20937  chtnprm  20939  shne0i  22952  pjneli  23227  eleigvec  23462  nmo  23975  qqhval2lem  24367  qqhval2  24368  sibfof  24656  dffr5  25378  wfi  25484  frind  25520  ellimits  25757  itg2addnclem2  26259  ftc1anclem3  26284  elicc3  26322  usgra2pthlem1  28336  onfrALTlem5  28690
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-ne 2603
  Copyright terms: Public domain W3C validator