# Metamath Proof Explorer

## Theorem cases2

Description: Case disjunction according to the value of ph . (Contributed by BJ, 6-Apr-2019) (Proof shortened by Wolf Lammen, 28-Feb-2022)

Ref Expression
Assertion cases2 ${⊢}\left(\left({\phi }\wedge {\psi }\right)\vee \left(¬{\phi }\wedge {\chi }\right)\right)↔\left(\left({\phi }\to {\psi }\right)\wedge \left(¬{\phi }\to {\chi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 pm4.83 ${⊢}\left(\left({\phi }\to \left(\left({\psi }\wedge {\phi }\right)\vee \left({\chi }\wedge ¬{\phi }\right)\right)\right)\wedge \left(¬{\phi }\to \left(\left({\psi }\wedge {\phi }\right)\vee \left({\chi }\wedge ¬{\phi }\right)\right)\right)\right)↔\left(\left({\psi }\wedge {\phi }\right)\vee \left({\chi }\wedge ¬{\phi }\right)\right)$
2 dedlema ${⊢}{\phi }\to \left({\psi }↔\left(\left({\psi }\wedge {\phi }\right)\vee \left({\chi }\wedge ¬{\phi }\right)\right)\right)$
3 2 pm5.74i ${⊢}\left({\phi }\to {\psi }\right)↔\left({\phi }\to \left(\left({\psi }\wedge {\phi }\right)\vee \left({\chi }\wedge ¬{\phi }\right)\right)\right)$
4 dedlemb ${⊢}¬{\phi }\to \left({\chi }↔\left(\left({\psi }\wedge {\phi }\right)\vee \left({\chi }\wedge ¬{\phi }\right)\right)\right)$
5 4 pm5.74i ${⊢}\left(¬{\phi }\to {\chi }\right)↔\left(¬{\phi }\to \left(\left({\psi }\wedge {\phi }\right)\vee \left({\chi }\wedge ¬{\phi }\right)\right)\right)$
6 3 5 anbi12i ${⊢}\left(\left({\phi }\to {\psi }\right)\wedge \left(¬{\phi }\to {\chi }\right)\right)↔\left(\left({\phi }\to \left(\left({\psi }\wedge {\phi }\right)\vee \left({\chi }\wedge ¬{\phi }\right)\right)\right)\wedge \left(¬{\phi }\to \left(\left({\psi }\wedge {\phi }\right)\vee \left({\chi }\wedge ¬{\phi }\right)\right)\right)\right)$
7 ancom ${⊢}\left({\phi }\wedge {\psi }\right)↔\left({\psi }\wedge {\phi }\right)$
8 ancom ${⊢}\left(¬{\phi }\wedge {\chi }\right)↔\left({\chi }\wedge ¬{\phi }\right)$
9 7 8 orbi12i ${⊢}\left(\left({\phi }\wedge {\psi }\right)\vee \left(¬{\phi }\wedge {\chi }\right)\right)↔\left(\left({\psi }\wedge {\phi }\right)\vee \left({\chi }\wedge ¬{\phi }\right)\right)$
10 1 6 9 3bitr4ri ${⊢}\left(\left({\phi }\wedge {\psi }\right)\vee \left(¬{\phi }\wedge {\chi }\right)\right)↔\left(\left({\phi }\to {\psi }\right)\wedge \left(¬{\phi }\to {\chi }\right)\right)$