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

Theorem necon3bbii 3063
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 225 . . 3 (𝐴 = 𝐵𝜑)
32necon3abii 3062 . 2 (𝐴𝐵 ↔ ¬ 𝜑)
43bicomi 225 1 𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  necon1abii  3064  nssinpss  4232  difsnpss  4734  xpdifid  6019  wfi  6175  ordintdif  6234  tfi  7556  oelim2  8211  0sdomg  8635  fin23lem26  9736  axdc3lem4  9864  axdc4lem  9866  axcclem  9868  crreczi  13579  ef0lem  15422  lidlnz  19931  nconnsubb  21961  ufileu  22457  itg2cnlem1  24291  plyeq0lem  24729  abelthlem2  24949  ppinprm  25657  chtnprm  25659  ltgov  26311  usgr2pthlem  27472  shne0i  29153  pjneli  29428  eleigvec  29662  nmo  30182  qqhval2lem  31122  qqhval2  31123  sibfof  31498  dffr5  32887  frpoind  32978  frind  32983  ellimits  33269  elicc3  33563  itg2addnclem2  34826  ftc1anclem3  34851  onfrALTlem5  40756  onfrALTlem5VD  41099  limcrecl  41790
  Copyright terms: Public domain W3C validator