Description: Eliminate a hypothesis containing class variable A when it is known for a specific class B . For more information, see comments in dedth . (Contributed by NM, 15-May-1999)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | elimhyp.1 | ⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜑 ↔ 𝜓 ) ) | |
| elimhyp.2 | ⊢ ( 𝐵 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜒 ↔ 𝜓 ) ) | ||
| elimhyp.3 | ⊢ 𝜒 | ||
| Assertion | elimhyp | ⊢ 𝜓 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elimhyp.1 | ⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | elimhyp.2 | ⊢ ( 𝐵 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜒 ↔ 𝜓 ) ) | |
| 3 | elimhyp.3 | ⊢ 𝜒 | |
| 4 | iftrue | ⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 ) | |
| 5 | 4 | eqcomd | ⊢ ( 𝜑 → 𝐴 = if ( 𝜑 , 𝐴 , 𝐵 ) ) |
| 6 | 5 1 | syl | ⊢ ( 𝜑 → ( 𝜑 ↔ 𝜓 ) ) |
| 7 | 6 | ibi | ⊢ ( 𝜑 → 𝜓 ) |
| 8 | iffalse | ⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 ) | |
| 9 | 8 | eqcomd | ⊢ ( ¬ 𝜑 → 𝐵 = if ( 𝜑 , 𝐴 , 𝐵 ) ) |
| 10 | 9 2 | syl | ⊢ ( ¬ 𝜑 → ( 𝜒 ↔ 𝜓 ) ) |
| 11 | 3 10 | mpbii | ⊢ ( ¬ 𝜑 → 𝜓 ) |
| 12 | 7 11 | pm2.61i | ⊢ 𝜓 |