Metamath Proof Explorer


Theorem 2alanimi

Description: Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011)

Ref Expression
Hypothesis 2alanimi.1 φ ψ χ
Assertion 2alanimi x y φ x y ψ x y χ

Proof

Step Hyp Ref Expression
1 2alanimi.1 φ ψ χ
2 1 alanimi y φ y ψ y χ
3 2 alanimi x y φ x y ψ x y χ