![]() |
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 1542 ≠ 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 206 df-ne 2941 |
This theorem is referenced by: pm2.61dane 3029 wefrc 5628 wereu2 5631 frpomin 6295 oe0lem 8460 fisupg 9238 marypha1lem 9374 fiinfg 9440 wdomtr 9516 unxpwdom2 9529 frmin 9690 fpwwe2lem12 10583 grur1a 10760 grutsk 10763 fimaxre2 12105 xlesubadd 13188 cshwidxmod 14697 sqreu 15251 pcxnn0cl 16737 pcxcl 16738 pcmpt 16769 symggen 19257 isabvd 20293 lspprat 20630 mdetralt 21973 ordtrest2lem 22570 ordthauslem 22750 comppfsc 22899 fbssint 23205 fclscf 23392 tgptsmscld 23518 ovoliunnul 24887 itg11 25071 i1fadd 25075 fta1g 25548 plydiveu 25674 fta1 25684 mulcxp 26056 cxpsqrt 26074 ostth3 27002 madebdaylemlrcut 27250 brbtwn2 27896 colinearalg 27901 clwwisshclwws 29001 ordtrest2NEWlem 32560 subfacp1lem5 33835 btwnexch2 34654 fnemeet2 34885 fnejoin2 34887 limsucncmpi 34963 areacirc 36217 sstotbnd2 36279 ssbnd 36293 prdsbnd2 36300 rrncmslem 36337 atnlt 37821 atlelt 37947 llnnlt 38032 lplnnlt 38074 lvolnltN 38127 pmapglb2N 38280 pmapglb2xN 38281 paddasslem14 38342 cdleme27a 38876 sdomne0 41773 sdomne0d 41774 iccpartigtl 45701 |
Copyright terms: Public domain | W3C validator |