Metamath Proof Explorer

Theorem axc16gb

Description: Biconditional strengthening of axc16g . (Contributed by NM, 15-May-1993)

Ref Expression
Assertion axc16gb 
|- ( A. x x = y -> ( ph <-> A. z ph ) )

Proof

Step Hyp Ref Expression
1 axc16g 
 |-  ( A. x x = y -> ( ph -> A. z ph ) )
2 sp 
 |-  ( A. z ph -> ph )
3 1 2 impbid1 
 |-  ( A. x x = y -> ( ph <-> A. z ph ) )