Metamath Proof Explorer


Theorem uun2221p2

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

Proof

Step Hyp Ref Expression
1 uun2221p2.1
 |-  ( ( ( ps /\ ph ) /\ ph /\ ph ) -> ch )
2 3anrev
 |-  ( ( ph /\ ph /\ ( ps /\ ph ) ) <-> ( ( ps /\ ph ) /\ ph /\ ph ) )
3 2 imbi1i
 |-  ( ( ( ph /\ ph /\ ( ps /\ ph ) ) -> ch ) <-> ( ( ( ps /\ ph ) /\ ph /\ ph ) -> ch ) )
4 1 3 mpbir
 |-  ( ( ph /\ ph /\ ( ps /\ ph ) ) -> ch )
5 3anass
 |-  ( ( ph /\ ph /\ ( ps /\ ph ) ) <-> ( ph /\ ( ph /\ ( ps /\ ph ) ) ) )
6 anabs5
 |-  ( ( ph /\ ( ph /\ ( ps /\ ph ) ) ) <-> ( ph /\ ( ps /\ ph ) ) )
7 5 6 bitri
 |-  ( ( ph /\ ph /\ ( ps /\ ph ) ) <-> ( ph /\ ( ps /\ ph ) ) )
8 ancom
 |-  ( ( ph /\ ps ) <-> ( ps /\ ph ) )
9 8 anbi2i
 |-  ( ( ph /\ ( ph /\ ps ) ) <-> ( ph /\ ( ps /\ ph ) ) )
10 7 9 bitr4i
 |-  ( ( ph /\ ph /\ ( ps /\ ph ) ) <-> ( ph /\ ( ph /\ ps ) ) )
11 anabs5
 |-  ( ( ph /\ ( ph /\ ps ) ) <-> ( ph /\ ps ) )
12 11 8 bitri
 |-  ( ( ph /\ ( ph /\ ps ) ) <-> ( ps /\ ph ) )
13 10 12 bitri
 |-  ( ( ph /\ ph /\ ( ps /\ ph ) ) <-> ( ps /\ ph ) )
14 13 imbi1i
 |-  ( ( ( ph /\ ph /\ ( ps /\ ph ) ) -> ch ) <-> ( ( ps /\ ph ) -> ch ) )
15 4 14 mpbi
 |-  ( ( ps /\ ph ) -> ch )