# Metamath Proof Explorer

## Theorem uun2131p1

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 uun2131p1.1 ${⊢}\left(\left({\phi }\wedge {\chi }\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\to {\theta }$
Assertion uun2131p1 ${⊢}\left({\phi }\wedge {\psi }\wedge {\chi }\right)\to {\theta }$

### Proof

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