| 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 3025 | 1 ⊢ (𝜑 → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ≠ wne 2940 |
| 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 207 df-ne 2941 |
| This theorem is referenced by: pm2.61dane 3029 wefrc 5679 wereu2 5682 frpomin 6361 oe0lem 8551 fisupg 9324 marypha1lem 9473 fiinfg 9539 wdomtr 9615 unxpwdom2 9628 frmin 9789 fpwwe2lem12 10682 grur1a 10859 grutsk 10862 fimaxre2 12213 xlesubadd 13305 cshwidxmod 14841 sqreu 15399 pcxnn0cl 16898 pcxcl 16899 pcmpt 16930 symggen 19488 isabvd 20813 lspprat 21155 mdetralt 22614 ordtrest2lem 23211 ordthauslem 23391 comppfsc 23540 fbssint 23846 fclscf 24033 tgptsmscld 24159 ovoliunnul 25542 itg11 25726 i1fadd 25730 fta1g 26209 plydiveu 26340 fta1 26350 mulcxp 26727 cxpsqrt 26745 ostth3 27682 madebdaylemlrcut 27937 brbtwn2 28920 colinearalg 28925 clwwisshclwws 30034 ordtrest2NEWlem 33921 subfacp1lem5 35189 btwnexch2 36024 fnemeet2 36368 fnejoin2 36370 limsucncmpi 36446 areacirc 37720 sstotbnd2 37781 ssbnd 37795 prdsbnd2 37802 rrncmslem 37839 atnlt 39314 atlelt 39440 llnnlt 39525 lplnnlt 39567 lvolnltN 39620 pmapglb2N 39773 pmapglb2xN 39774 paddasslem14 39835 cdleme27a 40369 sdomne0 43426 sdomne0d 43427 modelaxreplem1 44995 iccpartigtl 47410 |
| Copyright terms: Public domain | W3C validator |