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

Theorem necon3bbii 2988
Description: Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
Hypothesis
Ref Expression
necon3bbii.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
necon3bbii 𝜑𝐴𝐵)

Proof of Theorem necon3bbii
StepHypRef Expression
1 necon3bbii.1 . . . 4 (𝜑𝐴 = 𝐵)
21bicomi 224 . . 3 (𝐴 = 𝐵𝜑)
32necon3abii 2987 . 2 (𝐴𝐵 ↔ ¬ 𝜑)
43bicomi 224 1 𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206   = wceq 1540  wne 2940
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 207  df-ne 2941
This theorem is referenced by:  necon1abii  2989  nssinpss  4267  difsnpss  4807  xpdifid  6188  frpoind  6363  wfiOLD  6372  ordintdif  6434  tfi  7874  oelim2  8633  0sdomg  9144  0sdomgOLD  9145  frind  9790  fin23lem26  10365  axdc3lem4  10493  axdc4lem  10495  axcclem  10497  crreczi  14267  ef0lem  16114  lidlnz  21252  nconnsubb  23431  ufileu  23927  itg2cnlem1  25796  plyeq0lem  26249  abelthlem2  26476  ppinprm  27195  chtnprm  27197  sltlpss  27945  mulsval  28135  ltgov  28605  usgr2pthlem  29783  shne0i  31467  pjneli  31742  eleigvec  31976  nmo  32509  qqhval2lem  33982  qqhval2  33983  sibfof  34342  dffr5  35754  ellimits  35911  elicc3  36318  itg2addnclem2  37679  ftc1anclem3  37702  onfrALTlem5  44562  onfrALTlem5VD  44905  limcrecl  45644  dfnbgr6  47843
  Copyright terms: Public domain W3C validator