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 3020 | . . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
3 | pm2.61dne.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) | |
4 | 2, 3 | syl5bi 243 | . 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓)) |
5 | 1, 4 | pm2.61d 180 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = 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: pm2.61dane 3104 wefrc 5543 wereu2 5546 oe0lem 8129 fisupg 8755 marypha1lem 8886 fiinfg 8952 wdomtr 9028 unxpwdom2 9041 fpwwe2lem13 10053 grur1a 10230 grutsk 10233 fimaxre2 11575 xlesubadd 12646 cshwidxmod 14155 sqreu 14710 pcxcl 16187 pcmpt 16218 symggen 18529 isabvd 19522 lspprat 19856 mdetralt 21147 ordtrest2lem 21741 ordthauslem 21921 comppfsc 22070 fbssint 22376 fclscf 22563 tgptsmscld 22688 ovoliunnul 24037 itg11 24221 i1fadd 24225 fta1g 24690 plydiveu 24816 fta1 24826 mulcxp 25195 cxpsqrt 25213 ostth3 26142 brbtwn2 26619 colinearalg 26624 clwwisshclwws 27721 ordtrest2NEWlem 31065 subfacp1lem5 32329 frpomin 32976 frmin 32982 btwnexch2 33382 fnemeet2 33613 fnejoin2 33615 limsucncmpi 33691 areacirc 34869 sstotbnd2 34935 ssbnd 34949 prdsbnd2 34956 rrncmslem 34993 atnlt 36331 atlelt 36456 llnnlt 36541 lplnnlt 36583 lvolnltN 36636 pmapglb2N 36789 pmapglb2xN 36790 paddasslem14 36851 cdleme27a 37385 iccpartigtl 43430 |
Copyright terms: Public domain | W3C validator |