Metamath Proof Explorer


Theorem aaanv

Description: Theorem *11.56 in WhiteheadRussell p. 165. Special case of aaan . (Contributed by Andrew Salmon, 24-May-2011)

Ref Expression
Assertion aaanv x φ y ψ x y φ ψ

Proof

Step Hyp Ref Expression
1 nfv y φ
2 nfv x ψ
3 1 2 aaan x y φ ψ x φ y ψ
4 3 bicomi x φ y ψ x y φ ψ