![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.61dne | Structured version Visualization version GIF version |
Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
pm2.61dne.1 | ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) |
pm2.61dne.2 | ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) |
Ref | Expression |
---|---|
pm2.61dne | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.61dne.2 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) | |
2 | nne 2966 | . . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
3 | pm2.61dne.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) | |
4 | 2, 3 | syl5bi 234 | . 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓)) |
5 | 1, 4 | pm2.61d 172 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1508 ≠ wne 2962 |
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 199 df-ne 2963 |
This theorem is referenced by: pm2.61dane 3050 wefrc 5398 wereu2 5401 oe0lem 7939 fisupg 8560 marypha1lem 8691 fiinfg 8757 wdomtr 8833 unxpwdom2 8846 fpwwe2lem13 9861 grur1a 10038 grutsk 10041 fimaxre2 11386 xlesubadd 12471 cshwidxmod 14026 sqreu 14580 pcxcl 16052 pcmpt 16083 symggen 18372 isabvd 19326 lspprat 19660 mdetralt 20937 ordtrest2lem 21531 ordthauslem 21711 comppfsc 21860 fbssint 22166 fclscf 22353 tgptsmscld 22478 ovoliunnul 23827 itg11 24011 i1fadd 24015 fta1g 24480 plydiveu 24606 fta1 24616 mulcxp 24985 cxpsqrt 25003 ostth3 25932 brbtwn2 26410 colinearalg 26415 clwwisshclwws 27546 ordtrest2NEWlem 30842 subfacp1lem5 32049 frpomin 32632 frmin 32638 btwnexch2 33038 fnemeet2 33269 fnejoin2 33271 limsucncmpi 33346 areacirc 34461 sstotbnd2 34527 ssbnd 34541 prdsbnd2 34548 rrncmslem 34585 atnlt 35927 atlelt 36052 llnnlt 36137 lplnnlt 36179 lvolnltN 36232 pmapglb2N 36385 pmapglb2xN 36386 paddasslem14 36447 cdleme27a 36981 iccpartigtl 42985 |
Copyright terms: Public domain | W3C validator |