Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > necon3bbii | Structured version Visualization version GIF version |
Description: Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.) |
Ref | Expression |
---|---|
necon3bbii.1 | ⊢ (𝜑 ↔ 𝐴 = 𝐵) |
Ref | Expression |
---|---|
necon3bbii | ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3bbii.1 | . . . 4 ⊢ (𝜑 ↔ 𝐴 = 𝐵) | |
2 | 1 | bicomi 227 | . . 3 ⊢ (𝐴 = 𝐵 ↔ 𝜑) |
3 | 2 | necon3abii 2981 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) |
4 | 3 | bicomi 227 | 1 ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 = wceq 1543 ≠ wne 2935 |
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 210 df-ne 2936 |
This theorem is referenced by: necon1abii 2983 nssinpss 4161 difsnpss 4710 xpdifid 6020 frpoind 6185 wfi 6192 ordintdif 6251 tfi 7621 oelim2 8312 0sdomg 8764 frind 9355 fin23lem26 9922 axdc3lem4 10050 axdc4lem 10052 axcclem 10054 crreczi 13778 ef0lem 15621 lidlnz 20238 nconnsubb 22292 ufileu 22788 itg2cnlem1 24631 plyeq0lem 25076 abelthlem2 25296 ppinprm 26006 chtnprm 26008 ltgov 26660 usgr2pthlem 27822 shne0i 29501 pjneli 29776 eleigvec 30010 nmo 30529 qqhval2lem 31615 qqhval2 31616 sibfof 31991 dffr5 33408 sltlpss 33781 ellimits 33906 elicc3 34200 itg2addnclem2 35523 ftc1anclem3 35546 onfrALTlem5 41787 onfrALTlem5VD 42130 limcrecl 42799 |
Copyright terms: Public domain | W3C validator |