![]() |
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 4585. (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 4533 | . . . . 5 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
2 | 1 | eqcomd 2736 | . . . 4 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵)) |
3 | elimhyp.1 | . . . 4 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑 ↔ 𝜓)) | |
4 | 2, 3 | syl 17 | . . 3 ⊢ (𝜑 → (𝜑 ↔ 𝜓)) |
5 | 4 | ibi 266 | . 2 ⊢ (𝜑 → 𝜓) |
6 | elimhyp.3 | . . 3 ⊢ 𝜒 | |
7 | iffalse 4536 | . . . . 5 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | |
8 | 7 | eqcomd 2736 | . . . 4 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵)) |
9 | elimhyp.2 | . . . 4 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜓)) | |
10 | 8, 9 | syl 17 | . . 3 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜓)) |
11 | 6, 10 | mpbii 232 | . 2 ⊢ (¬ 𝜑 → 𝜓) |
12 | 5, 11 | pm2.61i 182 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 = wceq 1539 ifcif 4527 |
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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-if 4528 |
This theorem is referenced by: elimel 4596 elimf 6715 oeoa 8599 oeoe 8601 limensuc 9156 axcc4dom 10438 elimne0 11208 elimgt0 12056 elimge0 12057 2ndcdisj 23180 siilem2 30372 normlem7tALT 30639 hhsssh 30789 shintcl 30850 chintcl 30852 spanun 31065 elunop2 31533 lnophm 31539 nmbdfnlb 31570 hmopidmch 31673 hmopidmpj 31674 chirred 31915 limsucncmp 35634 elimhyps 38134 elimhyps2 38137 |
Copyright terms: Public domain | W3C validator |