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

Theorem necon3bbii 2829
 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 213 . . 3 (𝐴 = 𝐵𝜑)
32necon3abii 2828 . 2 (𝐴𝐵 ↔ ¬ 𝜑)
43bicomi 213 1 𝜑𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195   = wceq 1475   ≠ wne 2780 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 196  df-ne 2782 This theorem is referenced by:  necon1abii  2830  nssinpss  3818  difsnpss  4279  xpdifid  5481  wfi  5630  ordintdif  5691  tfi  6945  oelim2  7562  0sdomg  7974  fin23lem26  9030  axdc3lem4  9158  axdc4lem  9160  axcclem  9162  crreczi  12851  ef0lem  14648  lidlnz  19049  nconsubb  21036  ufileu  21533  itg2cnlem1  23334  plyeq0lem  23770  abelthlem2  23990  ppinprm  24678  chtnprm  24680  ltgov  25292  shne0i  27691  pjneli  27966  eleigvec  28200  nmo  28709  qqhval2lem  29353  qqhval2  29354  sibfof  29729  dffr5  30896  frind  30984  ellimits  31187  elicc3  31481  itg2addnclem2  32632  ftc1anclem3  32657  onfrALTlem5  37778  limcrecl  38696  usgr2pthlem  40969
 Copyright terms: Public domain W3C validator