![]() |
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 238 | . 2 ⊢ (𝐴 = 𝐵 → (𝜑 → 𝜓)) |
4 | pm2.61ne.2 | . . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) | |
5 | 4 | expcom 403 | . 2 ⊢ (𝐴 ≠ 𝐵 → (𝜑 → 𝜓)) |
6 | 3, 5 | pm2.61ine 3054 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 385 = wceq 1653 ≠ wne 2971 |
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 199 df-an 386 df-ne 2972 |
This theorem is referenced by: pwdom 8354 cantnfle 8818 cantnflem1 8836 cantnf 8840 cdalepw 9306 infmap2 9328 zornn0g 9615 ttukeylem6 9624 msqge0 10841 xrsupsslem 12386 xrinfmsslem 12387 fzoss1 12750 swrdcl 13669 pfxcl 13720 abs1m 14416 fsumcvg3 14801 bezoutlem4 15594 gcdmultiplez 15605 dvdssq 15615 lcmid 15657 pcdvdsb 15906 pcgcd1 15914 pc2dvds 15916 pcaddlem 15925 qexpz 15938 4sqlem19 16000 prmlem1a 16141 gsumwsubmcl 17690 gsumccat 17693 gsumwmhm 17698 zringlpir 20159 mretopd 21225 ufildom1 22058 alexsublem 22176 nmolb2d 22850 nmoi 22860 nmoix 22861 ipcau2 23360 mdegcl 24170 ply1divex 24237 ig1pcl 24276 dgrmulc 24368 mulcxplem 24771 vmacl 25196 efvmacl 25198 vmalelog 25282 padicabv 25671 nmlnoubi 28176 nmblolbii 28179 blocnilem 28184 blocni 28185 ubthlem1 28251 nmbdoplbi 29408 cnlnadjlem7 29457 branmfn 29489 pjbdlni 29533 shatomistici 29745 segcon2 32725 lssats 35033 ps-1 35498 3atlem5 35508 lplnnle2at 35562 2llnm3N 35590 lvolnle3at 35603 4atex2 36098 cdlemd5 36223 cdleme21k 36359 cdlemg33b 36728 mapdrvallem2 37666 mapdhcl 37748 hdmapval3N 37859 hdmap10 37861 hdmaprnlem17N 37884 hdmap14lem2a 37888 hdmaplkr 37934 hgmapvv 37947 cntzsdrg 38557 |
Copyright terms: Public domain | W3C validator |