Metamath Proof Explorer

Theorem alinexa

Description: A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993)

Ref Expression
Assertion alinexa x φ ¬ ψ ¬ x φ ψ


Step Hyp Ref Expression
1 imnang x φ ¬ ψ x ¬ φ ψ
2 alnex x ¬ φ ψ ¬ x φ ψ
3 1 2 bitri x φ ¬ ψ ¬ x φ ψ