Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elimhyp | Structured version Visualization version GIF version |
Description: Eliminate a hypothesis containing class variable 𝐴 when it is known for a specific class 𝐵. For more information, see comments in dedth 4516. (Contributed by NM, 15-May-1999.) |
Ref | Expression |
---|---|
elimhyp.1 | ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑 ↔ 𝜓)) |
elimhyp.2 | ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜓)) |
elimhyp.3 | ⊢ 𝜒 |
Ref | Expression |
---|---|
elimhyp | ⊢ 𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iftrue 4466 | . . . . 5 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
2 | 1 | eqcomd 2826 | . . . 4 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵)) |
3 | elimhyp.1 | . . . 4 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑 ↔ 𝜓)) | |
4 | 2, 3 | syl 17 | . . 3 ⊢ (𝜑 → (𝜑 ↔ 𝜓)) |
5 | 4 | ibi 269 | . 2 ⊢ (𝜑 → 𝜓) |
6 | elimhyp.3 | . . 3 ⊢ 𝜒 | |
7 | iffalse 4469 | . . . . 5 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | |
8 | 7 | eqcomd 2826 | . . . 4 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵)) |
9 | elimhyp.2 | . . . 4 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜓)) | |
10 | 8, 9 | syl 17 | . . 3 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜓)) |
11 | 6, 10 | mpbii 235 | . 2 ⊢ (¬ 𝜑 → 𝜓) |
12 | 5, 11 | pm2.61i 184 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 = wceq 1536 ifcif 4460 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-ext 2792 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ex 1780 df-sb 2069 df-clab 2799 df-cleq 2813 df-clel 2892 df-if 4461 |
This theorem is referenced by: elimel 4527 elimf 6506 oeoa 8216 oeoe 8218 limensuc 8687 axcc4dom 9856 elimne0 10624 elimgt0 11471 elimge0 11472 2ndcdisj 22059 siilem2 28627 normlem7tALT 28894 hhsssh 29044 shintcl 29105 chintcl 29107 spanun 29320 elunop2 29788 lnophm 29794 nmbdfnlb 29825 hmopidmch 29928 hmopidmpj 29929 chirred 30170 limsucncmp 33815 elimhyps 36130 elimhyps2 36133 |
Copyright terms: Public domain | W3C validator |