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

Metamath Proof Explorer

Theorem hba1w

Description: Weak version of hba1 . See comments for ax10w . Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017) (Proof shortened by Wolf Lammen, 10-Oct-2021)

Ref Expression
Hypothesis hbn1w.1 
|- ( x = y -> ( ph <-> ps ) )
Assertion hba1w 
|- ( A. x ph -> A. x A. x ph )

Proof

Step Hyp Ref Expression
1 hbn1w.1 
 |-  ( x = y -> ( ph <-> ps ) )
2 1 cbvalvw 
 |-  ( A. x ph <-> A. y ps )
3 2 notbii 
 |-  ( -. A. x ph <-> -. A. y ps )
4 3 a1i 
 |-  ( x = y -> ( -. A. x ph <-> -. A. y ps ) )
5 4 spw 
 |-  ( A. x -. A. x ph -> -. A. x ph )
6 5 con2i 
 |-  ( A. x ph -> -. A. x -. A. x ph )
7 4 hbn1w 
 |-  ( -. A. x -. A. x ph -> A. x -. A. x -. A. x ph )
8 1 hbn1w 
 |-  ( -. A. x ph -> A. x -. A. x ph )
9 8 con1i 
 |-  ( -. A. x -. A. x ph -> A. x ph )
10 9 alimi 
 |-  ( A. x -. A. x -. A. x ph -> A. x A. x ph )
11 6 7 10 3syl 
 |-  ( A. x ph -> A. x A. x ph )