Metamath Proof Explorer


Theorem wl-alanbii

Description: This theorem extends alanimi to a biconditional. Recurrent usage stacks up more quantifiers. (Contributed by Wolf Lammen, 4-Oct-2019)

Ref Expression
Hypothesis wl-alanbii.1
|- ( ph <-> ( ps /\ ch ) )
Assertion wl-alanbii
|- ( A. x ph <-> ( A. x ps /\ A. x ch ) )

Proof

Step Hyp Ref Expression
1 wl-alanbii.1
 |-  ( ph <-> ( ps /\ ch ) )
2 1 albii
 |-  ( A. x ph <-> A. x ( ps /\ ch ) )
3 19.26
 |-  ( A. x ( ps /\ ch ) <-> ( A. x ps /\ A. x ch ) )
4 2 3 bitri
 |-  ( A. x ph <-> ( A. x ps /\ A. x ch ) )