HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem necon3bbid 1592
Description: Deduction from equality to inequality.
Hypothesis
Ref Expression
necon3bbid.1 |- (ph -> (ps <-> A = B))
Assertion
Ref Expression
necon3bbid |- (ph -> (-. ps <-> A =/= B))
Proof of Theorem necon3bbid
StepHypRef Expression
1 necon3bbid.1 . . . 4 |- (ph -> (ps <-> A = B))
21bicomd 519 . . 3 |- (ph -> (A = B <-> ps))
32necon3abid 1591 . 2 |- (ph -> (A =/= B <-> -. ps))
43bicomd 519 1 |- (ph -> (-. ps <-> A =/= B))
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   = wceq 953   =/= wne 1577
This theorem is referenced by:  eldifsn 2453  php 4493  norm1ex 9043  lnfncon 9905
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 147  df-an 225  df-ne 1579
Copyright terms: Public domain