Metamath Proof Explorer


Theorem exanres2

Description: Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021)

Ref Expression
Assertion exanres2 B V C W u u R A B u S A C u A B u R C u S

Proof

Step Hyp Ref Expression
1 exanres B V C W u u R A B u S A C u A u R B u S C
2 exanres3 B V C W u A B u R C u S u A u R B u S C
3 1 2 bitr4d B V C W u u R A B u S A C u A B u R C u S