# Metamath Proof Explorer

## Theorem 3anandis

Description: Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 18-Apr-2007)

Ref Expression
Hypothesis 3anandis.1 ${⊢}\left(\left({\phi }\wedge {\psi }\right)\wedge \left({\phi }\wedge {\chi }\right)\wedge \left({\phi }\wedge {\theta }\right)\right)\to {\tau }$
Assertion 3anandis ${⊢}\left({\phi }\wedge \left({\psi }\wedge {\chi }\wedge {\theta }\right)\right)\to {\tau }$

### Proof

Step Hyp Ref Expression
1 3anandis.1 ${⊢}\left(\left({\phi }\wedge {\psi }\right)\wedge \left({\phi }\wedge {\chi }\right)\wedge \left({\phi }\wedge {\theta }\right)\right)\to {\tau }$
2 simpl ${⊢}\left({\phi }\wedge \left({\psi }\wedge {\chi }\wedge {\theta }\right)\right)\to {\phi }$
3 simpr1 ${⊢}\left({\phi }\wedge \left({\psi }\wedge {\chi }\wedge {\theta }\right)\right)\to {\psi }$
4 simpr2 ${⊢}\left({\phi }\wedge \left({\psi }\wedge {\chi }\wedge {\theta }\right)\right)\to {\chi }$
5 simpr3 ${⊢}\left({\phi }\wedge \left({\psi }\wedge {\chi }\wedge {\theta }\right)\right)\to {\theta }$
6 2 3 2 4 2 5 1 syl222anc ${⊢}\left({\phi }\wedge \left({\psi }\wedge {\chi }\wedge {\theta }\right)\right)\to {\tau }$