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

Metamath Proof Explorer

Theorem hbalw

Description: Weak version of hbal . Uses only Tarski's FOL axiom schemes. Unlike hbal , this theorem requires that x and y be distinct, i.e., not be bundled. (Contributed by NM, 19-Apr-2017)

Ref Expression
Hypotheses hbalw.1 
|- ( x = z -> ( ph <-> ps ) )
hbalw.2 
|- ( ph -> A. x ph )
Assertion hbalw 
|- ( A. y ph -> A. x A. y ph )

Proof

Step Hyp Ref Expression
1 hbalw.1 
 |-  ( x = z -> ( ph <-> ps ) )
2 hbalw.2 
 |-  ( ph -> A. x ph )
3 2 alimi 
 |-  ( A. y ph -> A. y A. x ph )
4 1 alcomimw 
 |-  ( A. y A. x ph -> A. x A. y ph )
5 3 4 syl 
 |-  ( A. y ph -> A. x A. y ph )