Metamath Proof Explorer

Theorem alinexa

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

Ref Expression
Assertion alinexa 
|- ( A. x ( ph -> -. ps ) <-> -. E. x ( ph /\ ps ) )

Proof

Step Hyp Ref Expression
1 imnang 
 |-  ( A. x ( ph -> -. ps ) <-> A. x -. ( ph /\ ps ) )
2 alnex 
 |-  ( A. x -. ( ph /\ ps ) <-> -. E. x ( ph /\ ps ) )
3 1 2 bitri 
 |-  ( A. x ( ph -> -. ps ) <-> -. E. x ( ph /\ ps ) )