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

Metamath Proof Explorer

Theorem ifboth

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

Ref Expression
Hypotheses ifboth.1 ⊢ A = if φ A B → ψ ↔ θ
ifboth.2 ⊢ B = if φ A B → χ ↔ θ
Assertion ifboth ⊢ ψ ∧ χ → θ

Proof

Step Hyp Ref Expression
1 ifboth.1 ⊢ A = if φ A B → ψ ↔ θ
2 ifboth.2 ⊢ B = if φ A B → χ ↔ θ
3 simpll ⊢ ψ ∧ χ ∧ φ → ψ
4 simplr ⊢ ψ ∧ χ ∧ ¬ φ → χ
5 1 2 3 4 ifbothda ⊢ ψ ∧ χ → θ