![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon3bbid | Structured version Visualization version GIF version |
Description: Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.) |
Ref | Expression |
---|---|
necon3bbid.1 | ⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵)) |
Ref | Expression |
---|---|
necon3bbid | ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3bbid.1 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵)) | |
2 | 1 | bicomd 222 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) |
3 | 2 | necon3abid 2967 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) |
4 | 3 | bicomd 222 | 1 ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 = wceq 1534 ≠ wne 2930 |
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 206 df-ne 2931 |
This theorem is referenced by: necon1abid 2969 necon3bid 2975 eldifsn 4785 php 9237 phpOLD 9249 xmullem2 13292 seqcoll2 14479 cnpart 15240 rlimrecl 15577 ncoprmgcdne1b 16646 prmrp 16708 4sqlem17 16958 mrieqvd 17646 mrieqv2d 17647 pltval 18352 latnlemlt 18492 latnle 18493 odnncl 19539 gexnnod 19582 sylow1lem1 19592 slwpss 19606 lssnle 19668 nzrunit 20502 imadrhmcl 20772 lspsnne1 21094 cnsubrg 21420 psrridm 21968 mhpmulcl 22139 cmpfi 23400 hausdiag 23637 txhaus 23639 isusp 24254 recld2 24818 metdseq0 24858 i1f1lem 25706 aaliou2b 26366 dvloglem 26672 logf1o2 26674 lgsne0 27361 lgsqr 27377 2sqlem7 27450 ostth3 27664 tglngne 28474 tgelrnln 28554 eucrct2eupth 30175 norm1exi 31180 atnemeq0 32307 opeldifid 32519 unitnz 33109 isdrng4 33152 pridln1 33324 mxidln1 33347 ssmxidllem 33354 rprmnz 33401 ply1unit 33453 ply1dg3rt0irred 33460 constrrtll 33604 qtophaus 33664 ordtconnlem1 33752 elzrhunit 33807 sgnneg 34387 subfacp1lem6 35026 maxidln1 37758 smprngopr 37766 lsatnem0 38756 atncmp 39023 atncvrN 39026 cdlema2N 39504 lhpmatb 39743 lhpat3 39758 cdleme3 39949 cdleme7 39961 cdlemg27b 40408 dvh2dimatN 41152 dvh2dim 41157 dochexmidlem1 41172 dochfln0 41189 dvrelog2b 41778 aks6d1c2p2 41831 hashscontpow 41834 rspcsbnea 41843 nna4b4nsq 42350 |
Copyright terms: Public domain | W3C validator |