Metamath Proof Explorer


Theorem exdistr

Description: Distribution of existential quantifiers. See also exdistrv . (Contributed by NM, 9-Mar-1995)

Ref Expression
Assertion exdistr xyφψxφyψ

Proof

Step Hyp Ref Expression
1 19.42v yφψφyψ
2 1 exbii xyφψxφyψ