# Metamath Proof Explorer

## Theorem elim2if

Description: Elimination of two conditional operators contained in a wff ch . (Contributed by Thierry Arnoux, 25-Jan-2017)

Ref Expression
Hypotheses elim2if.1 ${⊢}if\left({\phi },{A},if\left({\psi },{B},{C}\right)\right)={A}\to \left({\chi }↔{\theta }\right)$
elim2if.2 ${⊢}if\left({\phi },{A},if\left({\psi },{B},{C}\right)\right)={B}\to \left({\chi }↔{\tau }\right)$
elim2if.3 ${⊢}if\left({\phi },{A},if\left({\psi },{B},{C}\right)\right)={C}\to \left({\chi }↔{\eta }\right)$
Assertion elim2if ${⊢}{\chi }↔\left(\left({\phi }\wedge {\theta }\right)\vee \left(¬{\phi }\wedge \left(\left({\psi }\wedge {\tau }\right)\vee \left(¬{\psi }\wedge {\eta }\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 elim2if.1 ${⊢}if\left({\phi },{A},if\left({\psi },{B},{C}\right)\right)={A}\to \left({\chi }↔{\theta }\right)$
2 elim2if.2 ${⊢}if\left({\phi },{A},if\left({\psi },{B},{C}\right)\right)={B}\to \left({\chi }↔{\tau }\right)$
3 elim2if.3 ${⊢}if\left({\phi },{A},if\left({\psi },{B},{C}\right)\right)={C}\to \left({\chi }↔{\eta }\right)$
4 iftrue ${⊢}{\phi }\to if\left({\phi },{A},if\left({\psi },{B},{C}\right)\right)={A}$
5 4 1 syl ${⊢}{\phi }\to \left({\chi }↔{\theta }\right)$
6 iffalse ${⊢}¬{\phi }\to if\left({\phi },{A},if\left({\psi },{B},{C}\right)\right)=if\left({\psi },{B},{C}\right)$
7 6 eqeq1d ${⊢}¬{\phi }\to \left(if\left({\phi },{A},if\left({\psi },{B},{C}\right)\right)={B}↔if\left({\psi },{B},{C}\right)={B}\right)$
8 7 2 syl6bir ${⊢}¬{\phi }\to \left(if\left({\psi },{B},{C}\right)={B}\to \left({\chi }↔{\tau }\right)\right)$
9 6 eqeq1d ${⊢}¬{\phi }\to \left(if\left({\phi },{A},if\left({\psi },{B},{C}\right)\right)={C}↔if\left({\psi },{B},{C}\right)={C}\right)$
10 9 3 syl6bir ${⊢}¬{\phi }\to \left(if\left({\psi },{B},{C}\right)={C}\to \left({\chi }↔{\eta }\right)\right)$
11 8 10 elimifd ${⊢}¬{\phi }\to \left({\chi }↔\left(\left({\psi }\wedge {\tau }\right)\vee \left(¬{\psi }\wedge {\eta }\right)\right)\right)$
12 5 11 cases ${⊢}{\chi }↔\left(\left({\phi }\wedge {\theta }\right)\vee \left(¬{\phi }\wedge \left(\left({\psi }\wedge {\tau }\right)\vee \left(¬{\psi }\wedge {\eta }\right)\right)\right)\right)$