Metamath Proof Explorer

Theorem alrim3con13v

Description: Closed form of alrimi with 2 additional conjuncts having no occurrences of the quantifying variable. This proof is 19.21a3con13vVD automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion alrim3con13v 
|- ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( ps /\ ph /\ ch ) -> ps )
2 1 a1i 
 |-  ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> ps ) )
3 ax-5 
 |-  ( ps -> A. x ps )
4 2 3 syl6 
 |-  ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ps ) )
5 simp2 
 |-  ( ( ps /\ ph /\ ch ) -> ph )
6 5 imim1i 
 |-  ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ph ) )
7 simp3 
 |-  ( ( ps /\ ph /\ ch ) -> ch )
8 7 a1i 
 |-  ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> ch ) )
9 ax-5 
 |-  ( ch -> A. x ch )
10 8 9 syl6 
 |-  ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ch ) )
11 4 6 10 3jcad 
 |-  ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> ( A. x ps /\ A. x ph /\ A. x ch ) ) )
12 19.26-3an 
 |-  ( A. x ( ps /\ ph /\ ch ) <-> ( A. x ps /\ A. x ph /\ A. x ch ) )
13 11 12 imbitrrdi 
 |-  ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) )