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

Theorem necon3bbii 2979
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 2978 . 2 (𝐴𝐵 ↔ ¬ 𝜑)
43bicomi 214 1 𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196   = wceq 1632  wne 2932
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 2933
This theorem is referenced by:  necon1abii  2980  nssinpss  3999  difsnpss  4483  xpdifid  5720  wfi  5874  ordintdif  5935  tfi  7218  oelim2  7844  0sdomg  8254  fin23lem26  9339  axdc3lem4  9467  axdc4lem  9469  axcclem  9471  crreczi  13183  ef0lem  15008  lidlnz  19430  nconnsubb  21428  ufileu  21924  itg2cnlem1  23727  plyeq0lem  24165  abelthlem2  24385  ppinprm  25077  chtnprm  25079  ltgov  25691  usgr2pthlem  26869  shne0i  28616  pjneli  28891  eleigvec  29125  nmo  29634  qqhval2lem  30334  qqhval2  30335  sibfof  30711  dffr5  31950  frpoind  32046  frind  32049  ellimits  32323  elicc3  32617  itg2addnclem2  33775  ftc1anclem3  33800  onfrALTlem5  39259  onfrALTlem5VD  39620  limcrecl  40364
  Copyright terms: Public domain W3C validator