This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dedth4h

Description: Weak deduction theorem eliminating four hypotheses. See comments in dedth2h . (Contributed by NM, 16-May-1999)

Ref Expression
Hypotheses dedth4h.1 ⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝑅 ) → ( 𝜏 ↔ 𝜂 ) )
dedth4h.2 ⊢ ( 𝐵 = if ( 𝜓 , 𝐵 , 𝑆 ) → ( 𝜂 ↔ 𝜁 ) )
dedth4h.3 ⊢ ( 𝐶 = if ( 𝜒 , 𝐶 , 𝐹 ) → ( 𝜁 ↔ 𝜎 ) )
dedth4h.4 ⊢ ( 𝐷 = if ( 𝜃 , 𝐷 , 𝐺 ) → ( 𝜎 ↔ 𝜌 ) )
dedth4h.5 ⊢ 𝜌
Assertion dedth4h ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) → 𝜏 )

Proof

Step Hyp Ref Expression
1 dedth4h.1 ⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝑅 ) → ( 𝜏 ↔ 𝜂 ) )
2 dedth4h.2 ⊢ ( 𝐵 = if ( 𝜓 , 𝐵 , 𝑆 ) → ( 𝜂 ↔ 𝜁 ) )
3 dedth4h.3 ⊢ ( 𝐶 = if ( 𝜒 , 𝐶 , 𝐹 ) → ( 𝜁 ↔ 𝜎 ) )
4 dedth4h.4 ⊢ ( 𝐷 = if ( 𝜃 , 𝐷 , 𝐺 ) → ( 𝜎 ↔ 𝜌 ) )
5 dedth4h.5 ⊢ 𝜌
6 1 imbi2d ⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝑅 ) → ( ( ( 𝜒 ∧ 𝜃 ) → 𝜏 ) ↔ ( ( 𝜒 ∧ 𝜃 ) → 𝜂 ) ) )
7 2 imbi2d ⊢ ( 𝐵 = if ( 𝜓 , 𝐵 , 𝑆 ) → ( ( ( 𝜒 ∧ 𝜃 ) → 𝜂 ) ↔ ( ( 𝜒 ∧ 𝜃 ) → 𝜁 ) ) )
8 3 4 5 dedth2h ⊢ ( ( 𝜒 ∧ 𝜃 ) → 𝜁 )
9 6 7 8 dedth2h ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜒 ∧ 𝜃 ) → 𝜏 ) )
10 9 imp ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) → 𝜏 )