![]() |
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 4437. (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 4387 | . . . . 5 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
2 | 1 | eqcomd 2801 | . . . 4 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵)) |
3 | elimhyp.1 | . . . 4 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑 ↔ 𝜓)) | |
4 | 2, 3 | syl 17 | . . 3 ⊢ (𝜑 → (𝜑 ↔ 𝜓)) |
5 | 4 | ibi 268 | . 2 ⊢ (𝜑 → 𝜓) |
6 | elimhyp.3 | . . 3 ⊢ 𝜒 | |
7 | iffalse 4390 | . . . . 5 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | |
8 | 7 | eqcomd 2801 | . . . 4 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵)) |
9 | elimhyp.2 | . . . 4 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜓)) | |
10 | 8, 9 | syl 17 | . . 3 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜓)) |
11 | 6, 10 | mpbii 234 | . 2 ⊢ (¬ 𝜑 → 𝜓) |
12 | 5, 11 | pm2.61i 183 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 = wceq 1522 ifcif 4381 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-ex 1762 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-if 4382 |
This theorem is referenced by: elimel 4448 elimf 6381 oeoa 8073 oeoe 8075 limensuc 8541 axcc4dom 9709 elimne0 10477 elimgt0 11326 elimge0 11327 2ndcdisj 21748 siilem2 28320 normlem7tALT 28587 hhsssh 28737 shintcl 28798 chintcl 28800 spanun 29013 elunop2 29481 lnophm 29487 nmbdfnlb 29518 hmopidmch 29621 hmopidmpj 29622 chirred 29863 limsucncmp 33403 elimhyps 35628 elimhyps2 35631 |
Copyright terms: Public domain | W3C validator |