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

Metamath Proof Explorer

Theorem ifcld

Description: Membership (closure) of a conditional operator, deduction form. (Contributed by SO, 16-Jul-2018)

Ref Expression
Hypotheses ifcld.a ⊢ φ → A ∈ C
ifcld.b ⊢ φ → B ∈ C
Assertion ifcld ⊢ φ → if ψ A B ∈ C

Proof

Step Hyp Ref Expression
1 ifcld.a ⊢ φ → A ∈ C
2 ifcld.b ⊢ φ → B ∈ C
3 ifcl ⊢ A ∈ C ∧ B ∈ C → if ψ A B ∈ C
4 1 2 3 syl2anc ⊢ φ → if ψ A B ∈ C