Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > necon3abid | Structured version Visualization version GIF version |
Description: Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.) |
Ref | Expression |
---|---|
necon3abid.1 | ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) |
Ref | Expression |
---|---|
necon3abid | ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 3017 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | necon3abid.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) | |
3 | 2 | notbid 319 | . 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝜓)) |
4 | 1, 3 | syl5bb 284 | 1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 = wceq 1528 ≠ wne 3016 |
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 208 df-ne 3017 |
This theorem is referenced by: necon3bbid 3053 necon2abid 3058 prnesn 4784 foconst 6597 fndmdif 6805 suppsnop 7835 om00el 8192 oeoa 8213 cardsdom2 9406 mulne0b 11270 crne0 11620 expneg 13427 hashsdom 13732 prprrab 13821 gcdn0gt0 15856 cncongr2 16002 pltval3 17567 mulgnegnn 18178 drngmulne0 19455 lvecvsn0 19812 domnmuln0 20001 mvrf1 20135 connsub 21959 pthaus 22176 xkohaus 22191 bndth 23491 lebnumlem1 23494 dvcobr 24472 dvcnvlem 24502 mdegle0 24600 coemulhi 24773 vieta1lem1 24828 vieta1lem2 24829 aalioulem2 24851 cosne0 25041 atandm3 25383 wilthlem2 25574 issqf 25641 mumullem2 25685 dchrptlem3 25770 lgseisenlem3 25881 brbtwn2 26619 colinearalg 26624 vdn0conngrumgrv2 27903 vdgn1frgrv2 28003 nmlno0lem 28498 nmlnop0iALT 29700 atcvat2i 30092 divnumden2 30461 lindssn 30867 fedgmullem2 30926 bnj1542 32029 bnj1253 32187 ptrecube 34774 poimirlem13 34787 ecinn0 35490 llnexchb2 36887 cdlemb3 37624 rencldnfilem 39297 qirropth 39385 binomcxplemfrat 40563 binomcxplemradcnv 40564 odz2prm2pw 43572 |
Copyright terms: Public domain | W3C validator |