This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uun2221

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

Ref Expression
Hypothesis uun2221.1 
|- ( ( ph /\ ph /\ ( ps /\ ph ) ) -> ch )
Assertion uun2221 
|- ( ( ps /\ ph ) -> ch )

Proof

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