# Metamath Proof Explorer

## Theorem mpjao3danOLD

Description: Obsolete version of mpjao3dan as of 17-Apr-2024. (Contributed by Thierry Arnoux, 13-Apr-2018) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses mpjao3dan.1 ${⊢}\left({\phi }\wedge {\psi }\right)\to {\chi }$
mpjao3dan.2 ${⊢}\left({\phi }\wedge {\theta }\right)\to {\chi }$
mpjao3dan.3 ${⊢}\left({\phi }\wedge {\tau }\right)\to {\chi }$
mpjao3dan.4 ${⊢}{\phi }\to \left({\psi }\vee {\theta }\vee {\tau }\right)$
Assertion mpjao3danOLD ${⊢}{\phi }\to {\chi }$

### Proof

Step Hyp Ref Expression
1 mpjao3dan.1 ${⊢}\left({\phi }\wedge {\psi }\right)\to {\chi }$
2 mpjao3dan.2 ${⊢}\left({\phi }\wedge {\theta }\right)\to {\chi }$
3 mpjao3dan.3 ${⊢}\left({\phi }\wedge {\tau }\right)\to {\chi }$
4 mpjao3dan.4 ${⊢}{\phi }\to \left({\psi }\vee {\theta }\vee {\tau }\right)$
5 1 2 jaodan ${⊢}\left({\phi }\wedge \left({\psi }\vee {\theta }\right)\right)\to {\chi }$
6 df-3or ${⊢}\left({\psi }\vee {\theta }\vee {\tau }\right)↔\left(\left({\psi }\vee {\theta }\right)\vee {\tau }\right)$
7 4 6 sylib ${⊢}{\phi }\to \left(\left({\psi }\vee {\theta }\right)\vee {\tau }\right)$
8 5 3 7 mpjaodan ${⊢}{\phi }\to {\chi }$