Metamath Proof Explorer

Theorem imnang

Description: Quantified implication in terms of quantified negation of conjunction. (Contributed by BJ, 16-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 imnan 
 |-  ( ( ph -> -. ps ) <-> -. ( ph /\ ps ) )
2 1 albii 
 |-  ( A. x ( ph -> -. ps ) <-> A. x -. ( ph /\ ps ) )