Metamath Proof Explorer


Theorem bj-pm11.53vw

Description: Version of pm11.53v with nonfreeness antecedents. One can also prove the theorem with antecedent ( F// y A. x ph /\ A. y F// x ps ) . (Contributed by BJ, 7-Oct-2024)

Ref Expression
Assertion bj-pm11.53vw x Ⅎ' y φ Ⅎ' x y ψ x y φ ψ x φ y ψ

Proof

Step Hyp Ref Expression
1 simpl x Ⅎ' y φ Ⅎ' x y ψ x Ⅎ' y φ
2 bj-19.21t Ⅎ' y φ y φ ψ φ y ψ
3 1 2 sylg x Ⅎ' y φ Ⅎ' x y ψ x y φ ψ φ y ψ
4 albi x y φ ψ φ y ψ x y φ ψ x φ y ψ
5 3 4 syl x Ⅎ' y φ Ⅎ' x y ψ x y φ ψ x φ y ψ
6 bj-19.23t Ⅎ' x y ψ x φ y ψ x φ y ψ
7 6 adantl x Ⅎ' y φ Ⅎ' x y ψ x φ y ψ x φ y ψ
8 5 7 bitrd x Ⅎ' y φ Ⅎ' x y ψ x y φ ψ x φ y ψ