Theorem necon3bbii 2841

Description: Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)

Hypothesis

Ref	Expression
necon3bbii.1	|- ( ph <-> A = B )

Assertion

Ref	Expression
necon3bbii	|- ( -. ph <-> A =/= B )

Proof of Theorem necon3bbii

Step	Hyp	Ref	Expression
1		necon3bbii.1	. . . 4 |- ( ph <-> A = B )
2	1	bicomi 214	. . 3 |- ( A = B <-> ph )
3	2	necon3abii 2840	. 2 |- ( A =/= B <-> -. ph )
4	3	bicomi 214	1 |- ( -. ph <-> A =/= B )

Syntax hints:   -. wn 3   <-> wb 196   = wceq 1483   =/= wne 2794

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 2795

This theorem is referenced by:  necon1abii  2842  nssinpss  3856  difsnpss  4338  xpdifid  5562  wfi  5713  ordintdif  5774  tfi  7053  oelim2  7675  0sdomg  8089  fin23lem26  9147  axdc3lem4  9275  axdc4lem  9277  axcclem  9279  crreczi  12989  ef0lem  14809  lidlnz  19228  nconnsubb  21226  ufileu  21723  itg2cnlem1  23528  plyeq0lem  23966  abelthlem2  24186  ppinprm  24878  chtnprm  24880  ltgov  25492  usgr2pthlem  26659  shne0i  28307  pjneli  28582  eleigvec  28816  nmo  29325  qqhval2lem  30025  qqhval2  30026  sibfof  30402  dffr5  31643  frind  31740  ellimits  32017  elicc3  32311  itg2addnclem2  33462  ftc1anclem3  33487  onfrALTlem5  38757  limcrecl  39861