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 2939 | . . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
3 | pm2.61dne.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) | |
4 | 2, 3 | syl5bi 245 | . 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓)) |
5 | 1, 4 | pm2.61d 182 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1543 ≠ wne 2935 |
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 210 df-ne 2936 |
This theorem is referenced by: pm2.61dane 3022 wefrc 5534 wereu2 5537 frpomin 6183 oe0lem 8229 fisupg 8908 marypha1lem 9038 fiinfg 9104 wdomtr 9180 unxpwdom2 9193 frmin 9354 fpwwe2lem12 10239 grur1a 10416 grutsk 10419 fimaxre2 11760 xlesubadd 12836 cshwidxmod 14351 sqreu 14907 pcxnn0cl 16394 pcxcl 16395 pcmpt 16426 symggen 18834 isabvd 19828 lspprat 20162 mdetralt 21477 ordtrest2lem 22072 ordthauslem 22252 comppfsc 22401 fbssint 22707 fclscf 22894 tgptsmscld 23020 ovoliunnul 24376 itg11 24560 i1fadd 24564 fta1g 25037 plydiveu 25163 fta1 25173 mulcxp 25545 cxpsqrt 25563 ostth3 26491 brbtwn2 26968 colinearalg 26973 clwwisshclwws 28070 ordtrest2NEWlem 31558 subfacp1lem5 32831 madebdaylemlrcut 33773 btwnexch2 34019 fnemeet2 34250 fnejoin2 34252 limsucncmpi 34328 areacirc 35564 sstotbnd2 35626 ssbnd 35640 prdsbnd2 35647 rrncmslem 35684 atnlt 37021 atlelt 37146 llnnlt 37231 lplnnlt 37273 lvolnltN 37326 pmapglb2N 37479 pmapglb2xN 37480 paddasslem14 37541 cdleme27a 38075 iccpartigtl 44502 |
Copyright terms: Public domain | W3C validator |