Metamath Proof Explorer


Theorem ralnex3

Description: Relationship between three restricted universal and existential quantifiers. (Contributed by Thierry Arnoux, 12-Jul-2020) (Proof shortened by Wolf Lammen, 18-May-2023)

Ref Expression
Assertion ralnex3 x A y B z C ¬ φ ¬ x A y B z C φ

Proof

Step Hyp Ref Expression
1 ralnex z C ¬ φ ¬ z C φ
2 1 2ralbii x A y B z C ¬ φ x A y B ¬ z C φ
3 ralnex2 x A y B ¬ z C φ ¬ x A y B z C φ
4 2 3 bitri x A y B z C ¬ φ ¬ x A y B z C φ