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

Theorem necon3bbii 2631
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 2630 . 2  |-  ( A  =/=  B  <->  -.  ph )
43bicomi 202 1  |-  ( -. 
ph 
<->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    = wceq 1364    =/= 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:  nssinpss  3572  difsnpss  4006  ordintdif  4757  xpdifid  5256  tfi  6455  oelim2  7024  0sdomg  7430  fin23lem26  8484  axdc3lem4  8612  axdc4lem  8614  axcclem  8616  crreczi  11975  ef0lem  13349  lidlnz  17234  nconsubb  18871  ufileu  19336  itg2cnlem1  21083  plyeq0lem  21565  abelthlem2  21784  ppinprm  22377  chtnprm  22379  shne0i  24676  pjneli  24951  eleigvec  25186  nmo  25695  qqhval2lem  26266  qqhval2  26267  sibfof  26576  dffr5  27412  wfi  27517  frind  27553  ellimits  27790  itg2addnclem2  28290  ftc1anclem3  28315  elicc3  28358  usgra2pthlem1  30148  onfrALTlem5  30991
  Copyright terms: Public domain W3C validator