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

Metamath Proof Explorer

Theorem ifbothda

Description: A wff th containing a conditional operator is true when both of its cases are true. (Contributed by NM, 15-Feb-2015)

Ref Expression
Hypotheses ifboth.1 ⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜓 ↔ 𝜃 ) )
ifboth.2 ⊢ ( 𝐵 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜒 ↔ 𝜃 ) )
ifbothda.3 ⊢ ( ( 𝜂 ∧ 𝜑 ) → 𝜓 )
ifbothda.4 ⊢ ( ( 𝜂 ∧ ¬ 𝜑 ) → 𝜒 )
Assertion ifbothda ( 𝜂 → 𝜃 )

Proof

Step Hyp Ref Expression
1 ifboth.1 ⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜓 ↔ 𝜃 ) )
2 ifboth.2 ⊢ ( 𝐵 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜒 ↔ 𝜃 ) )
3 ifbothda.3 ⊢ ( ( 𝜂 ∧ 𝜑 ) → 𝜓 )
4 ifbothda.4 ⊢ ( ( 𝜂 ∧ ¬ 𝜑 ) → 𝜒 )
5 iftrue ⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 )
6 5 eqcomd ⊢ ( 𝜑 → 𝐴 = if ( 𝜑 , 𝐴 , 𝐵 ) )
7 6 1 syl ⊢ ( 𝜑 → ( 𝜓 ↔ 𝜃 ) )
8 7 adantl ⊢ ( ( 𝜂 ∧ 𝜑 ) → ( 𝜓 ↔ 𝜃 ) )
9 3 8 mpbid ⊢ ( ( 𝜂 ∧ 𝜑 ) → 𝜃 )
10 iffalse ⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 )
11 10 eqcomd ⊢ ( ¬ 𝜑 → 𝐵 = if ( 𝜑 , 𝐴 , 𝐵 ) )
12 11 2 syl ⊢ ( ¬ 𝜑 → ( 𝜒 ↔ 𝜃 ) )
13 12 adantl ⊢ ( ( 𝜂 ∧ ¬ 𝜑 ) → ( 𝜒 ↔ 𝜃 ) )
14 4 13 mpbid ⊢ ( ( 𝜂 ∧ ¬ 𝜑 ) → 𝜃 )
15 9 14 pm2.61dan ⊢ ( 𝜂 → 𝜃 )