Metamath Proof Explorer


Theorem 3anidm12p2

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 3anidm12p2.1
|- ( ( ps /\ ph /\ ph ) -> ch )
Assertion 3anidm12p2
|- ( ( ph /\ ps ) -> ch )

Proof

Step Hyp Ref Expression
1 3anidm12p2.1
 |-  ( ( ps /\ ph /\ ph ) -> ch )
2 3anrot
 |-  ( ( ps /\ ph /\ ph ) <-> ( ph /\ ph /\ ps ) )
3 2 1 sylbir
 |-  ( ( ph /\ ph /\ ps ) -> ch )
4 3 3anidm12
 |-  ( ( ph /\ ps ) -> ch )