Theorem necon3abii 2993

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

Hypothesis

Ref	Expression
necon3abii.1	⊢ (𝐴 = 𝐵 ↔ 𝜑)

Assertion

Ref	Expression
necon3abii	⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑)

Proof of Theorem necon3abii

Step	Hyp	Ref	Expression
1		df-ne 2947	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3abii.1	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝜑)
3	1, 2	xchbinx 334	1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1537   ≠ wne 2946

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 207  df-ne 2947

This theorem is referenced by:  necon3bbii  2994  necon3bii  2999  nesym  3003  rabn0  4412  dffr6  5655  xpimasn  6218  rankxplim3  9952  rankxpsuc  9953  dflt2  13212  gcd0id  16567  lcmfunsnlem2  16689  axlowdimlem13  28989  hashxpe  32816  ssdifidllem  33451  ssmxidllem  33468  fedgmullem2  33645  gonanegoal  35322  filnetlem4  36349  dihatlat  41293  sn-00id  42379  pellex  42793  nev  43734  ldepspr  48204