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
|- ( ( ( ph /\ ch ) /\ ( ph /\ ps ) ) -> th )
Assertion uun2131p1
|- ( ( ph /\ ps /\ ch ) -> th )

Proof

Step Hyp Ref Expression
1 uun2131p1.1
 |-  ( ( ( ph /\ ch ) /\ ( ph /\ ps ) ) -> th )
2 ancom
 |-  ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) <-> ( ( ph /\ ch ) /\ ( ph /\ ps ) ) )
3 2 1 sylbi
 |-  ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) -> th )
4 3 3impdi
 |-  ( ( ph /\ ps /\ ch ) -> th )