| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > pm2.61ne | Structured version Visualization version GIF version | ||
| Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
| Ref | Expression |
|---|---|
| pm2.61ne.1 | ⊢ (𝐴 = 𝐵 → (𝜓 ↔ 𝜒)) |
| pm2.61ne.2 | ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) |
| pm2.61ne.3 | ⊢ (𝜑 → 𝜒) |
| Ref | Expression |
|---|---|
| pm2.61ne | ⊢ (𝜑 → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm2.61ne.3 | . . 3 ⊢ (𝜑 → 𝜒) | |
| 2 | pm2.61ne.1 | . . 3 ⊢ (𝐴 = 𝐵 → (𝜓 ↔ 𝜒)) | |
| 3 | 1, 2 | imbitrrid 246 | . 2 ⊢ (𝐴 = 𝐵 → (𝜑 → 𝜓)) |
| 4 | pm2.61ne.2 | . . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) | |
| 5 | 4 | expcom 413 | . 2 ⊢ (𝐴 ≠ 𝐵 → (𝜑 → 𝜓)) |
| 6 | 3, 5 | pm2.61ine 3025 | 1 ⊢ (𝜑 → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = 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-an 396 df-ne 2941 |
| This theorem is referenced by: pwdom 9169 cantnfle 9711 cantnflem1 9729 cantnf 9733 djulepw 10233 infmap2 10257 zornn0g 10545 ttukeylem6 10554 msqge0 11784 xrsupsslem 13349 xrinfmsslem 13350 fzoss1 13726 swrdcl 14683 pfxcl 14715 abs1m 15374 fsumcvg3 15765 bezoutlem4 16579 dvdssq 16604 lcmid 16646 pcdvdsb 16907 pcgcd1 16915 pc2dvds 16917 pcaddlem 16926 qexpz 16939 4sqlem19 17001 prmlem1a 17144 gsumwsubmcl 18850 gsumccat 18854 gsumwmhm 18858 cntzsdrg 20803 zringlpir 21478 psdmul 22170 mretopd 23100 ufildom1 23934 alexsublem 24052 nmolb2d 24739 nmoi 24749 nmoix 24750 ipcau2 25268 mdegcl 26108 ply1divex 26176 ig1pcl 26218 dgrmulc 26311 mulcxplem 26726 vmacl 27161 efvmacl 27163 vmalelog 27249 padicabv 27674 nmlnoubi 30815 nmblolbii 30818 blocnilem 30823 blocni 30824 ubthlem1 30889 nmbdoplbi 32043 cnlnadjlem7 32092 branmfn 32124 pjbdlni 32168 shatomistici 32380 segcon2 36106 lssats 39013 ps-1 39479 3atlem5 39489 lplnnle2at 39543 2llnm3N 39571 lvolnle3at 39584 4atex2 40079 cdlemd5 40204 cdleme21k 40340 cdlemg33b 40709 mapdrvallem2 41647 mapdhcl 41729 hdmapval3N 41840 hdmap10 41842 hdmaprnlem17N 41865 hdmap14lem2a 41869 hdmaplkr 41915 hgmapvv 41928 explt1d 42358 fiabv 42546 |
| Copyright terms: Public domain | W3C validator |