Metamath Proof Explorer


Theorem r19.41

Description: Restricted quantifier version of 19.41 . See r19.41v for a version with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 1-Nov-2010)

Ref Expression
Hypothesis r19.41.1 x ψ
Assertion r19.41 x A φ ψ x A φ ψ

Proof

Step Hyp Ref Expression
1 r19.41.1 x ψ
2 anass x A φ ψ x A φ ψ
3 2 exbii x x A φ ψ x x A φ ψ
4 1 19.41 x x A φ ψ x x A φ ψ
5 3 4 bitr3i x x A φ ψ x x A φ ψ
6 df-rex x A φ ψ x x A φ ψ
7 df-rex x A φ x x A φ
8 7 anbi1i x A φ ψ x x A φ ψ
9 5 6 8 3bitr4i x A φ ψ x A φ ψ