# Metamath Proof Explorer

## Theorem ifclda

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

Ref Expression
Hypotheses ifclda.1 ${⊢}\left({\phi }\wedge {\psi }\right)\to {A}\in {C}$
ifclda.2 ${⊢}\left({\phi }\wedge ¬{\psi }\right)\to {B}\in {C}$
Assertion ifclda ${⊢}{\phi }\to if\left({\psi },{A},{B}\right)\in {C}$

### Proof

Step Hyp Ref Expression
1 ifclda.1 ${⊢}\left({\phi }\wedge {\psi }\right)\to {A}\in {C}$
2 ifclda.2 ${⊢}\left({\phi }\wedge ¬{\psi }\right)\to {B}\in {C}$
3 iftrue ${⊢}{\psi }\to if\left({\psi },{A},{B}\right)={A}$
4 3 adantl ${⊢}\left({\phi }\wedge {\psi }\right)\to if\left({\psi },{A},{B}\right)={A}$
5 4 1 eqeltrd ${⊢}\left({\phi }\wedge {\psi }\right)\to if\left({\psi },{A},{B}\right)\in {C}$
6 iffalse ${⊢}¬{\psi }\to if\left({\psi },{A},{B}\right)={B}$
7 6 adantl ${⊢}\left({\phi }\wedge ¬{\psi }\right)\to if\left({\psi },{A},{B}\right)={B}$
8 7 2 eqeltrd ${⊢}\left({\phi }\wedge ¬{\psi }\right)\to if\left({\psi },{A},{B}\right)\in {C}$
9 5 8 pm2.61dan ${⊢}{\phi }\to if\left({\psi },{A},{B}\right)\in {C}$