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 | syl5ibr 235 | . 2 ⊢ (𝐴 = 𝐵 → (𝜑 → 𝜓)) |
4 | pm2.61ne.2 | . . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) | |
5 | 4 | expcom 450 | . 2 ⊢ (𝐴 ≠ 𝐵 → (𝜑 → 𝜓)) |
6 | 3, 5 | pm2.61ine 2865 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ≠ wne 2780 |
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 196 df-an 385 df-ne 2782 |
This theorem is referenced by: pwdom 7997 cantnfle 8451 cantnflem1 8469 cantnf 8473 cdalepw 8901 infmap2 8923 zornn0g 9210 ttukeylem6 9219 msqge0 10428 xrsupsslem 12009 xrinfmsslem 12010 fzoss1 12364 swrdcl 13271 abs1m 13923 fsumcvg3 14307 bezoutlem4 15097 gcdmultiplez 15108 dvdssq 15118 lcmid 15160 pcdvdsb 15411 pcgcd1 15419 pc2dvds 15421 pcaddlem 15430 qexpz 15443 4sqlem19 15505 prmlem1a 15651 gsumwsubmcl 17198 gsumccat 17201 gsumwmhm 17205 zringlpir 19656 mretopd 20706 ufildom1 21540 alexsublem 21658 nmolb2d 22332 nmoi 22342 nmoix 22343 ipcau2 22841 mdegcl 23633 ply1divex 23700 ig1pcl 23739 dgrmulc 23831 mulcxplem 24230 vmacl 24644 efvmacl 24646 vmalelog 24730 padicabv 25119 nmlnoubi 27035 nmblolbii 27038 blocnilem 27043 blocni 27044 ubthlem1 27110 nmbdoplbi 28267 cnlnadjlem7 28316 branmfn 28348 pjbdlni 28392 shatomistici 28604 segcon2 31382 lssats 33317 ps-1 33781 3atlem5 33791 lplnnle2at 33845 2llnm3N 33873 lvolnle3at 33886 4atex2 34381 cdlemd5 34507 cdleme21k 34644 cdlemg33b 35013 mapdrvallem2 35952 mapdhcl 36034 hdmapval3N 36148 hdmap10 36150 hdmaprnlem17N 36173 hdmap14lem2a 36177 hdmaplkr 36223 hgmapvv 36236 cntzsdrg 36791 pfxcl 40249 |
Copyright terms: Public domain | W3C validator |