Metamath Proof Explorer

Theorem bj-axc16g16

Description: Proof of axc16g from { ax-1 -- ax-7 , axc16 }. (Contributed by BJ, 6-Jul-2021) (Proof modification is discouraged.)

Ref Expression
Assertion bj-axc16g16 
|- ( A. x x = y -> ( ph -> A. z ph ) )

Proof

Step Hyp Ref Expression
1 aevlem 
 |-  ( A. x x = y -> A. z z = t )
2 axc16 
 |-  ( A. z z = t -> ( ph -> A. z ph ) )
3 1 2 syl 
 |-  ( A. x x = y -> ( ph -> A. z ph ) )