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

Metamath Proof Explorer

Theorem ax13dgen4

Description: Degenerate instance of ax-13 where bundled variables x , y , and z have a common substitution. Therefore, also a degenerate instance of ax13dgen1 , ax13dgen2 , and ax13dgen3 . Also an instance of the intuitionistic tautology pm2.21 . Uses only Tarski's FOL axiom schemes. (Contributed by NM, 13-Apr-2017) Reduce axiom usage. (Revised by Wolf Lammen, 10-Oct-2021)

Ref Expression
Assertion ax13dgen4 
|- ( -. x = x -> ( x = x -> A. x x = x ) )

Proof

Step Hyp Ref Expression
1 pm2.21 
 |-  ( -. x = x -> ( x = x -> A. x x = x ) )