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

Metamath Proof Explorer

Theorem spc3gv

Description: Specialization with three quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008)

Ref Expression
Hypothesis spc3egv.1 
|- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )
Assertion spc3gv 
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A. x A. y A. z ph -> ps ) )

Proof

Step Hyp Ref Expression
1 spc3egv.1 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )
2 1 notbid 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( -. ph <-> -. ps ) )
3 2 spc3egv 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( -. ps -> E. x E. y E. z -. ph ) )
4 exnal 
 |-  ( E. z -. ph <-> -. A. z ph )
5 4 exbii 
 |-  ( E. y E. z -. ph <-> E. y -. A. z ph )
6 exnal 
 |-  ( E. y -. A. z ph <-> -. A. y A. z ph )
7 5 6 bitri 
 |-  ( E. y E. z -. ph <-> -. A. y A. z ph )
8 7 exbii 
 |-  ( E. x E. y E. z -. ph <-> E. x -. A. y A. z ph )
9 exnal 
 |-  ( E. x -. A. y A. z ph <-> -. A. x A. y A. z ph )
10 8 9 bitr2i 
 |-  ( -. A. x A. y A. z ph <-> E. x E. y E. z -. ph )
11 3 10 imbitrrdi 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( -. ps -> -. A. x A. y A. z ph ) )
12 11 con4d 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A. x A. y A. z ph -> ps ) )