Metamath Proof Explorer


Theorem pm5.31r

Description: Variant of pm5.31 . (Contributed by Rodolfo Medina, 15-Oct-2010)

Ref Expression
Assertion pm5.31r χφψφχψ

Proof

Step Hyp Ref Expression
1 ax-1 χφχ
2 id φψφψ
3 1 2 anim12ii χφψφχψ