# Metamath Proof Explorer

## Theorem wl-orel12

Description: In a conjunctive normal form a pair of nodes like ( ph \/ ps ) /\ ( -. ph \/ ch ) eliminates the need of a node ( ps \/ ch ) . This theorem allows simplifications in that respect. (Contributed by Wolf Lammen, 20-Jun-2020)

Ref Expression
Assertion wl-orel12 ${⊢}\left(\left({\phi }\vee {\psi }\right)\wedge \left(¬{\phi }\vee {\chi }\right)\right)\to \left({\psi }\vee {\chi }\right)$

### Proof

Step Hyp Ref Expression
1 pm2.1 ${⊢}\left(¬{\phi }\vee {\phi }\right)$
2 orel1 ${⊢}¬{\phi }\to \left(\left({\phi }\vee {\psi }\right)\to {\psi }\right)$
3 orc ${⊢}{\psi }\to \left({\psi }\vee {\chi }\right)$
4 2 3 syl6com ${⊢}\left({\phi }\vee {\psi }\right)\to \left(¬{\phi }\to \left({\psi }\vee {\chi }\right)\right)$
5 notnot ${⊢}{\phi }\to ¬¬{\phi }$
6 orel1 ${⊢}¬¬{\phi }\to \left(\left(¬{\phi }\vee {\chi }\right)\to {\chi }\right)$
7 5 6 syl ${⊢}{\phi }\to \left(\left(¬{\phi }\vee {\chi }\right)\to {\chi }\right)$
8 olc ${⊢}{\chi }\to \left({\psi }\vee {\chi }\right)$
9 7 8 syl6com ${⊢}\left(¬{\phi }\vee {\chi }\right)\to \left({\phi }\to \left({\psi }\vee {\chi }\right)\right)$
10 4 9 jaao ${⊢}\left(\left({\phi }\vee {\psi }\right)\wedge \left(¬{\phi }\vee {\chi }\right)\right)\to \left(\left(¬{\phi }\vee {\phi }\right)\to \left({\psi }\vee {\chi }\right)\right)$
11 1 10 mpi ${⊢}\left(\left({\phi }\vee {\psi }\right)\wedge \left(¬{\phi }\vee {\chi }\right)\right)\to \left({\psi }\vee {\chi }\right)$