Description: Weak deduction theorem for eliminating a hypothesis with 4 class variables. See comments in dedth2v . (Contributed by NM, 21-Apr-2007) (Proof shortened by Eric Schmidt, 28-Jul-2009)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dedth4v.1 | ⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝑅 ) → ( 𝜓 ↔ 𝜒 ) ) | |
| dedth4v.2 | ⊢ ( 𝐵 = if ( 𝜑 , 𝐵 , 𝑆 ) → ( 𝜒 ↔ 𝜃 ) ) | ||
| dedth4v.3 | ⊢ ( 𝐶 = if ( 𝜑 , 𝐶 , 𝑇 ) → ( 𝜃 ↔ 𝜏 ) ) | ||
| dedth4v.4 | ⊢ ( 𝐷 = if ( 𝜑 , 𝐷 , 𝑈 ) → ( 𝜏 ↔ 𝜂 ) ) | ||
| dedth4v.5 | ⊢ 𝜂 | ||
| Assertion | dedth4v | ⊢ ( 𝜑 → 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dedth4v.1 | ⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝑅 ) → ( 𝜓 ↔ 𝜒 ) ) | |
| 2 | dedth4v.2 | ⊢ ( 𝐵 = if ( 𝜑 , 𝐵 , 𝑆 ) → ( 𝜒 ↔ 𝜃 ) ) | |
| 3 | dedth4v.3 | ⊢ ( 𝐶 = if ( 𝜑 , 𝐶 , 𝑇 ) → ( 𝜃 ↔ 𝜏 ) ) | |
| 4 | dedth4v.4 | ⊢ ( 𝐷 = if ( 𝜑 , 𝐷 , 𝑈 ) → ( 𝜏 ↔ 𝜂 ) ) | |
| 5 | dedth4v.5 | ⊢ 𝜂 | |
| 6 | 1 2 3 4 5 | dedth4h | ⊢ ( ( ( 𝜑 ∧ 𝜑 ) ∧ ( 𝜑 ∧ 𝜑 ) ) → 𝜓 ) |
| 7 | 6 | anidms | ⊢ ( ( 𝜑 ∧ 𝜑 ) → 𝜓 ) |
| 8 | 7 | anidms | ⊢ ( 𝜑 → 𝜓 ) |