Metamath Proof Explorer


Theorem rexnal3

Description: Relationship between three restricted universal and existential quantifiers. (Contributed by Thierry Arnoux, 12-Jul-2020)

Ref Expression
Assertion rexnal3 xAyBzC¬φ¬xAyBzCφ

Proof

Step Hyp Ref Expression
1 rexnal zC¬φ¬zCφ
2 1 2rexbii xAyBzC¬φxAyB¬zCφ
3 rexnal2 xAyB¬zCφ¬xAyBzCφ
4 2 3 bitri xAyBzC¬φ¬xAyBzCφ