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 247 | . 2 ⊢ (𝐴 = 𝐵 → (𝜑 → 𝜓)) |
4 | pm2.61ne.2 | . . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) | |
5 | 4 | expcom 414 | . 2 ⊢ (𝐴 ≠ 𝐵 → (𝜑 → 𝜓)) |
6 | 3, 5 | pm2.61ine 3100 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1528 ≠ wne 3016 |
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 208 df-an 397 df-ne 3017 |
This theorem is referenced by: pwdom 8658 cantnfle 9123 cantnflem1 9141 cantnf 9145 djulepw 9607 infmap2 9629 zornn0g 9916 ttukeylem6 9925 msqge0 11150 xrsupsslem 12690 xrinfmsslem 12691 fzoss1 13054 swrdcl 13997 pfxcl 14029 abs1m 14685 fsumcvg3 15076 bezoutlem4 15880 gcdmultiplezOLD 15891 dvdssq 15901 lcmid 15943 pcdvdsb 16195 pcgcd1 16203 pc2dvds 16205 pcaddlem 16214 qexpz 16227 4sqlem19 16289 prmlem1a 16430 gsumwsubmcl 17991 gsumccatOLD 17995 gsumccat 17996 gsumwmhm 18000 cntzsdrg 19512 zringlpir 20566 mretopd 21630 ufildom1 22464 alexsublem 22582 nmolb2d 23256 nmoi 23266 nmoix 23267 ipcau2 23766 mdegcl 24592 ply1divex 24659 ig1pcl 24698 dgrmulc 24790 mulcxplem 25194 vmacl 25623 efvmacl 25625 vmalelog 25709 padicabv 26134 nmlnoubi 28501 nmblolbii 28504 blocnilem 28509 blocni 28510 ubthlem1 28575 nmbdoplbi 29729 cnlnadjlem7 29778 branmfn 29810 pjbdlni 29854 shatomistici 30066 segcon2 33464 lssats 36030 ps-1 36495 3atlem5 36505 lplnnle2at 36559 2llnm3N 36587 lvolnle3at 36600 4atex2 37095 cdlemd5 37220 cdleme21k 37356 cdlemg33b 37725 mapdrvallem2 38663 mapdhcl 38745 hdmapval3N 38856 hdmap10 38858 hdmaprnlem17N 38881 hdmap14lem2a 38885 hdmaplkr 38931 hgmapvv 38944 |
Copyright terms: Public domain | W3C validator |