Metamath Proof Explorer


Theorem pm11.53v

Description: Version of pm11.53 with a disjoint variable condition, requiring fewer axioms. (Contributed by BJ, 7-Mar-2020)

Ref Expression
Assertion pm11.53v xyφψxφyψ

Proof

Step Hyp Ref Expression
1 19.21v yφψφyψ
2 1 albii xyφψxφyψ
3 19.23v xφyψxφyψ
4 2 3 bitri xyφψxφyψ