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

Theorem necon3bbii 3037
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 227 . . 3 (𝐴 = 𝐵𝜑)
32necon3abii 3036 . 2 (𝐴𝐵 ↔ ¬ 𝜑)
43bicomi 227 1 𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209   = wceq 1538  wne 2990
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 210  df-ne 2991
This theorem is referenced by:  necon1abii  3038  nssinpss  4186  difsnpss  4703  xpdifid  5996  wfi  6153  ordintdif  6212  tfi  7552  oelim2  8208  0sdomg  8634  fin23lem26  9740  axdc3lem4  9868  axdc4lem  9870  axcclem  9872  crreczi  13589  ef0lem  15427  lidlnz  19997  nconnsubb  22031  ufileu  22527  itg2cnlem1  24368  plyeq0lem  24810  abelthlem2  25030  ppinprm  25740  chtnprm  25742  ltgov  26394  usgr2pthlem  27555  shne0i  29234  pjneli  29509  eleigvec  29743  nmo  30264  qqhval2lem  31330  qqhval2  31331  sibfof  31706  dffr5  33097  frpoind  33188  frind  33193  ellimits  33479  elicc3  33773  itg2addnclem2  35102  ftc1anclem3  35125  onfrALTlem5  41235  onfrALTlem5VD  41578  limcrecl  42258
  Copyright terms: Public domain W3C validator