Metamath Proof Explorer


Theorem bj-nnfext

Description: See nfex and bj-nfext . (Contributed by BJ, 12-Aug-2023) (Proof modification is discouraged.)

Ref Expression
Assertion bj-nnfext x Ⅎ' y φ Ⅎ' y x φ

Proof

Step Hyp Ref Expression
1 df-bj-nnf Ⅎ' y φ y φ φ φ y φ
2 1 albii x Ⅎ' y φ x y φ φ φ y φ
3 simpl y φ φ φ y φ y φ φ
4 3 alimi x y φ φ φ y φ x y φ φ
5 bj-nnflemee x y φ φ y x φ x φ
6 4 5 syl x y φ φ φ y φ y x φ x φ
7 2 6 sylbi x Ⅎ' y φ y x φ x φ
8 simpr y φ φ φ y φ φ y φ
9 8 alimi x y φ φ φ y φ x φ y φ
10 bj-nnflemae x φ y φ x φ y x φ
11 9 10 syl x y φ φ φ y φ x φ y x φ
12 2 11 sylbi x Ⅎ' y φ x φ y x φ
13 df-bj-nnf Ⅎ' y x φ y x φ x φ x φ y x φ
14 7 12 13 sylanbrc x Ⅎ' y φ Ⅎ' y x φ