Metamath Proof Explorer


Theorem pm10.55

Description: Theorem *10.55 in WhiteheadRussell p. 156. (Contributed by Andrew Salmon, 24-May-2011)

Ref Expression
Assertion pm10.55 xφψxφψxφxφψ

Proof

Step Hyp Ref Expression
1 exsimpl xφψxφ
2 1 anim1i xφψxφψxφxφψ
3 exintr xφψxφxφψ
4 3 imdistanri xφxφψxφψxφψ
5 2 4 impbii xφψxφψxφxφψ