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

Theorem necon3bbii 2870
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 214 . . 3 (𝐴 = 𝐵𝜑)
32necon3abii 2869 . 2 (𝐴𝐵 ↔ ¬ 𝜑)
43bicomi 214 1 𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196   = wceq 1523  wne 2823
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 197  df-ne 2824
This theorem is referenced by:  necon1abii  2871  nssinpss  3889  difsnpss  4370  xpdifid  5597  wfi  5751  ordintdif  5812  tfi  7095  oelim2  7720  0sdomg  8130  fin23lem26  9185  axdc3lem4  9313  axdc4lem  9315  axcclem  9317  crreczi  13029  ef0lem  14853  lidlnz  19276  nconnsubb  21274  ufileu  21770  itg2cnlem1  23573  plyeq0lem  24011  abelthlem2  24231  ppinprm  24923  chtnprm  24925  ltgov  25537  usgr2pthlem  26715  shne0i  28435  pjneli  28710  eleigvec  28944  nmo  29453  qqhval2lem  30153  qqhval2  30154  sibfof  30530  dffr5  31769  frpoind  31865  frind  31868  ellimits  32142  elicc3  32436  itg2addnclem2  33592  ftc1anclem3  33617  onfrALTlem5  39074  onfrALTlem5VD  39435  limcrecl  40179
  Copyright terms: Public domain W3C validator