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 ⊢ A = if φ A B → ψ ↔ θ
ifboth.2 ⊢ B = if φ A B → χ ↔ θ
ifbothda.3 ⊢ η ∧ φ → ψ
ifbothda.4 ⊢ η ∧ ¬ φ → χ
Assertion ifbothda ⊢ η → θ

Proof

Step Hyp Ref Expression
1 ifboth.1 ⊢ A = if φ A B → ψ ↔ θ
2 ifboth.2 ⊢ B = if φ A B → χ ↔ θ
3 ifbothda.3 ⊢ η ∧ φ → ψ
4 ifbothda.4 ⊢ η ∧ ¬ φ → χ
5 iftrue ⊢ φ → if φ A B = A
6 5 eqcomd ⊢ φ → A = if φ A B
7 6 1 syl ⊢ φ → ψ ↔ θ
8 7 adantl ⊢ η ∧ φ → ψ ↔ θ
9 3 8 mpbid ⊢ η ∧ φ → θ
10 iffalse ⊢ ¬ φ → if φ A B = B
11 10 eqcomd ⊢ ¬ φ → B = if φ A B
12 11 2 syl ⊢ ¬ φ → χ ↔ θ
13 12 adantl ⊢ η ∧ ¬ φ → χ ↔ θ
14 4 13 mpbid ⊢ η ∧ ¬ φ → θ
15 9 14 pm2.61dan ⊢ η → θ