Metamath Proof Explorer


Theorem pm11.59

Description: Theorem *11.59 in WhiteheadRussell p. 165. (Contributed by Andrew Salmon, 25-May-2011)

Ref Expression
Assertion pm11.59 xφψyxφyxφψyxψ

Proof

Step Hyp Ref Expression
1 nfv yφψ
2 1 nfal yxφψ
3 sp xφψφψ
4 spsbim xφψyxφyxψ
5 3 4 anim12d xφψφyxφψyxψ
6 5 axc4i xφψxφyxφψyxψ
7 2 6 alrimi xφψyxφyxφψyxψ