# Metamath Proof Explorer

## Theorem uun132p1

Description: A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017) (Proof modification is discouraged.) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 uun132p1.1 ${⊢}\left(\left({\psi }\wedge {\chi }\right)\wedge {\phi }\right)\to {\theta }$
2 3anass ${⊢}\left({\phi }\wedge {\psi }\wedge {\chi }\right)↔\left({\phi }\wedge \left({\psi }\wedge {\chi }\right)\right)$
3 ancom ${⊢}\left({\phi }\wedge \left({\psi }\wedge {\chi }\right)\right)↔\left(\left({\psi }\wedge {\chi }\right)\wedge {\phi }\right)$
4 2 3 bitri ${⊢}\left({\phi }\wedge {\psi }\wedge {\chi }\right)↔\left(\left({\psi }\wedge {\chi }\right)\wedge {\phi }\right)$
5 4 1 sylbi ${⊢}\left({\phi }\wedge {\psi }\wedge {\chi }\right)\to {\theta }$