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

Theorem necon3bbii 2477
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 193 . . 3  |-  ( A  =  B  <->  ph )
32necon3abii 2476 . 2  |-  ( A  =/=  B  <->  -.  ph )
43bicomi 193 1  |-  ( -. 
ph 
<->  A  =/=  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    = wceq 1623    =/= wne 2446
This theorem is referenced by:  nssinpss  3401  difsnpss  3758  ordintdif  4441  tfi  4644  oelim2  6593  0sdomg  6990  fin23lem26  7951  axdc3lem4  8079  axdc4lem  8081  axcclem  8083  crreczi  11226  ef0lem  12360  lidlnz  15980  nconsubb  17149  ufileu  17614  itg2cnlem1  19116  plyeq0lem  19592  abelthlem2  19808  isosctrlem1  20118  ppinprm  20390  chtnprm  20392  shne0i  22027  pjneli  22302  eleigvec  22537  dffr5  23521  wfi  23618  frind  23654  ellimits  23861  nbssntrs  25559  elicc3  25640  onfrALTlem5  27680
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 177  df-ne 2448
  Copyright terms: Public domain W3C validator