Metamath Proof Explorer


Theorem nfralwOLD

Description: Obsolete version of nfralw as of 13-Dec-2024. (Contributed by NM, 1-Sep-1999) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses nfralw.1 _ x A
nfralw.2 x φ
Assertion nfralwOLD x y A φ

Proof

Step Hyp Ref Expression
1 nfralw.1 _ x A
2 nfralw.2 x φ
3 nftru y
4 1 a1i _ x A
5 2 a1i x φ
6 3 4 5 nfraldw x y A φ
7 6 mptru x y A φ