![]() |
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 415 | . 2 ⊢ (𝐴 ≠ 𝐵 → (𝜑 → 𝜓)) |
6 | 3, 5 | pm2.61ine 3025 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = 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-an 398 df-ne 2941 |
This theorem is referenced by: pwdom 9076 cantnfle 9612 cantnflem1 9630 cantnf 9634 djulepw 10133 infmap2 10159 zornn0g 10446 ttukeylem6 10455 msqge0 11681 xrsupsslem 13232 xrinfmsslem 13233 fzoss1 13605 swrdcl 14539 pfxcl 14571 abs1m 15226 fsumcvg3 15619 bezoutlem4 16428 dvdssq 16448 lcmid 16490 pcdvdsb 16746 pcgcd1 16754 pc2dvds 16756 pcaddlem 16765 qexpz 16778 4sqlem19 16840 prmlem1a 16984 gsumwsubmcl 18652 gsumccat 18656 gsumwmhm 18660 cntzsdrg 20283 zringlpir 20904 mretopd 22459 ufildom1 23293 alexsublem 23411 nmolb2d 24098 nmoi 24108 nmoix 24109 ipcau2 24614 mdegcl 25450 ply1divex 25517 ig1pcl 25556 dgrmulc 25648 mulcxplem 26055 vmacl 26483 efvmacl 26485 vmalelog 26569 padicabv 26994 nmlnoubi 29780 nmblolbii 29783 blocnilem 29788 blocni 29789 ubthlem1 29854 nmbdoplbi 31008 cnlnadjlem7 31057 branmfn 31089 pjbdlni 31133 shatomistici 31345 segcon2 34736 lssats 37520 ps-1 37986 3atlem5 37996 lplnnle2at 38050 2llnm3N 38078 lvolnle3at 38091 4atex2 38586 cdlemd5 38711 cdleme21k 38847 cdlemg33b 39216 mapdrvallem2 40154 mapdhcl 40236 hdmapval3N 40347 hdmap10 40349 hdmaprnlem17N 40372 hdmap14lem2a 40376 hdmaplkr 40422 hgmapvv 40435 |
Copyright terms: Public domain | W3C validator |