![]() |
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 245 | . 2 ⊢ (𝐴 = 𝐵 → (𝜑 → 𝜓)) |
4 | pm2.61ne.2 | . . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) | |
5 | 4 | expcom 412 | . 2 ⊢ (𝐴 ≠ 𝐵 → (𝜑 → 𝜓)) |
6 | 3, 5 | pm2.61ine 3014 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1533 ≠ wne 2929 |
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-an 395 df-ne 2930 |
This theorem is referenced by: pwdom 9157 cantnfle 9701 cantnflem1 9719 cantnf 9723 djulepw 10222 infmap2 10248 zornn0g 10535 ttukeylem6 10544 msqge0 11772 xrsupsslem 13326 xrinfmsslem 13327 fzoss1 13699 swrdcl 14639 pfxcl 14671 abs1m 15326 fsumcvg3 15719 bezoutlem4 16529 dvdssq 16554 lcmid 16596 pcdvdsb 16857 pcgcd1 16865 pc2dvds 16867 pcaddlem 16876 qexpz 16889 4sqlem19 16951 prmlem1a 17095 gsumwsubmcl 18813 gsumccat 18817 gsumwmhm 18821 cntzsdrg 20719 zringlpir 21427 psdmul 22130 mretopd 23057 ufildom1 23891 alexsublem 24009 nmolb2d 24696 nmoi 24706 nmoix 24707 ipcau2 25223 mdegcl 26066 ply1divex 26134 ig1pcl 26175 dgrmulc 26268 mulcxplem 26680 vmacl 27115 efvmacl 27117 vmalelog 27203 padicabv 27628 nmlnoubi 30698 nmblolbii 30701 blocnilem 30706 blocni 30707 ubthlem1 30772 nmbdoplbi 31926 cnlnadjlem7 31975 branmfn 32007 pjbdlni 32051 shatomistici 32263 segcon2 35852 lssats 38634 ps-1 39100 3atlem5 39110 lplnnle2at 39164 2llnm3N 39192 lvolnle3at 39205 4atex2 39700 cdlemd5 39825 cdleme21k 39961 cdlemg33b 40330 mapdrvallem2 41268 mapdhcl 41350 hdmapval3N 41461 hdmap10 41463 hdmaprnlem17N 41486 hdmap14lem2a 41490 hdmaplkr 41536 hgmapvv 41549 |
Copyright terms: Public domain | W3C validator |