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 3017 | . . 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 3013 |
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 3014 |
This theorem is referenced by: pm2.61dane 3101 wefrc 5542 wereu2 5545 oe0lem 8127 fisupg 8754 marypha1lem 8885 fiinfg 8951 wdomtr 9027 unxpwdom2 9040 fpwwe2lem13 10052 grur1a 10229 grutsk 10232 fimaxre2 11574 xlesubadd 12644 cshwidxmod 14153 sqreu 14708 pcxcl 16185 pcmpt 16216 symggen 18527 isabvd 19520 lspprat 19854 mdetralt 21145 ordtrest2lem 21739 ordthauslem 21919 comppfsc 22068 fbssint 22374 fclscf 22561 tgptsmscld 22686 ovoliunnul 24035 itg11 24219 i1fadd 24223 fta1g 24688 plydiveu 24814 fta1 24824 mulcxp 25195 cxpsqrt 25213 ostth3 26141 brbtwn2 26618 colinearalg 26623 clwwisshclwws 27720 ordtrest2NEWlem 31064 subfacp1lem5 32328 frpomin 32975 frmin 32981 btwnexch2 33381 fnemeet2 33612 fnejoin2 33614 limsucncmpi 33690 areacirc 34868 sstotbnd2 34933 ssbnd 34947 prdsbnd2 34954 rrncmslem 34991 atnlt 36329 atlelt 36454 llnnlt 36539 lplnnlt 36581 lvolnltN 36634 pmapglb2N 36787 pmapglb2xN 36788 paddasslem14 36849 cdleme27a 37383 iccpartigtl 43460 |
Copyright terms: Public domain | W3C validator |