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

Metamath Proof Explorer

Theorem r19.26

Description: Restricted quantifier version of 19.26 . (Contributed by NM, 28-Jan-1997) (Proof shortened by Andrew Salmon, 30-May-2011)

Ref Expression
Assertion r19.26 
|- ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. x e. A ps ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( ph /\ ps ) -> ph )
2 1 ralimi 
 |-  ( A. x e. A ( ph /\ ps ) -> A. x e. A ph )
3 simpr 
 |-  ( ( ph /\ ps ) -> ps )
4 3 ralimi 
 |-  ( A. x e. A ( ph /\ ps ) -> A. x e. A ps )
5 2 4 jca 
 |-  ( A. x e. A ( ph /\ ps ) -> ( A. x e. A ph /\ A. x e. A ps ) )
6 pm3.2 
 |-  ( ph -> ( ps -> ( ph /\ ps ) ) )
7 6 ral2imi 
 |-  ( A. x e. A ph -> ( A. x e. A ps -> A. x e. A ( ph /\ ps ) ) )
8 7 imp 
 |-  ( ( A. x e. A ph /\ A. x e. A ps ) -> A. x e. A ( ph /\ ps ) )
9 5 8 impbii 
 |-  ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. x e. A ps ) )