![]() |
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.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) | |
2 | 1 | com12 32 | . 2 ⊢ (𝐴 = 𝐵 → (𝜑 → 𝜓)) |
3 | pm2.61dne.2 | . . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) | |
4 | 3 | com12 32 | . 2 ⊢ (𝐴 ≠ 𝐵 → (𝜑 → 𝜓)) |
5 | 2, 4 | pm2.61ine 3015 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 ≠ wne 2930 |
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 206 df-ne 2931 |
This theorem is referenced by: pm2.61dane 3019 wefrc 5668 wereu2 5671 frpomin 6345 oe0lem 8535 fisupg 9318 marypha1lem 9469 fiinfg 9535 wdomtr 9611 unxpwdom2 9624 frmin 9785 fpwwe2lem12 10676 grur1a 10853 grutsk 10856 fimaxre2 12205 xlesubadd 13290 cshwidxmod 14806 sqreu 15360 pcxnn0cl 16857 pcxcl 16858 pcmpt 16889 symggen 19464 isabvd 20787 lspprat 21130 mdetralt 22598 ordtrest2lem 23195 ordthauslem 23375 comppfsc 23524 fbssint 23830 fclscf 24017 tgptsmscld 24143 ovoliunnul 25524 itg11 25708 i1fadd 25712 fta1g 26194 plydiveu 26323 fta1 26333 mulcxp 26709 cxpsqrt 26727 ostth3 27664 madebdaylemlrcut 27919 brbtwn2 28836 colinearalg 28841 clwwisshclwws 29945 ordtrest2NEWlem 33750 subfacp1lem5 35025 btwnexch2 35860 fnemeet2 36092 fnejoin2 36094 limsucncmpi 36170 areacirc 37427 sstotbnd2 37488 ssbnd 37502 prdsbnd2 37509 rrncmslem 37546 atnlt 39024 atlelt 39150 llnnlt 39235 lplnnlt 39277 lvolnltN 39330 pmapglb2N 39483 pmapglb2xN 39484 paddasslem14 39545 cdleme27a 40079 sdomne0 43117 sdomne0d 43118 iccpartigtl 47031 |
Copyright terms: Public domain | W3C validator |