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

Metamath Proof Explorer

Theorem ifclda

Description: Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypotheses ifclda.1 ⊢ φ ∧ ψ → A ∈ C
ifclda.2 ⊢ φ ∧ ¬ ψ → B ∈ C
Assertion ifclda ⊢ φ → if ψ A B ∈ C

Proof

Step Hyp Ref Expression
1 ifclda.1 ⊢ φ ∧ ψ → A ∈ C
2 ifclda.2 ⊢ φ ∧ ¬ ψ → B ∈ C
3 iftrue ⊢ ψ → if ψ A B = A
4 3 adantl ⊢ φ ∧ ψ → if ψ A B = A
5 4 1 eqeltrd ⊢ φ ∧ ψ → if ψ A B ∈ C
6 iffalse ⊢ ¬ ψ → if ψ A B = B
7 6 adantl ⊢ φ ∧ ¬ ψ → if ψ A B = B
8 7 2 eqeltrd ⊢ φ ∧ ¬ ψ → if ψ A B ∈ C
9 5 8 pm2.61dan ⊢ φ → if ψ A B ∈ C