Metamath Proof Explorer


Theorem hbsbwOLD

Description: Obsolete version of hbsbw as of 23-May-2024. (Contributed by NM, 12-Aug-1993) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis hbsbwOLD.1 φ z φ
Assertion hbsbwOLD y x φ z y x φ

Proof

Step Hyp Ref Expression
1 hbsbwOLD.1 φ z φ
2 1 nf5i z φ
3 2 nfsbv z y x φ
4 3 nf5ri y x φ z y x φ