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

Metamath Proof Explorer

Theorem 19.16

Description: Theorem 19.16 of Margaris p. 90. (Contributed by NM, 12-Mar-1993)

Ref Expression
Hypothesis 19.16.1 
|- F/ x ph
Assertion 19.16 
|- ( A. x ( ph <-> ps ) -> ( ph <-> A. x ps ) )

Proof

Step Hyp Ref Expression
1 19.16.1 
 |-  F/ x ph
2 1 19.3 
 |-  ( A. x ph <-> ph )
3 albi 
 |-  ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) )
4 2 3 bitr3id 
 |-  ( A. x ( ph <-> ps ) -> ( ph <-> A. x ps ) )