Metamath Proof Explorer


Theorem ralrexbidOLD

Description: Obsolete version of ralrexbid as of 4-Nov-2024. (Contributed by AV, 21-Oct-2023) Reduce axiom usage. (Revised by SN, 13-Nov-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis ralrexbid.1 φ ψ θ
Assertion ralrexbidOLD x A φ x A ψ x A θ

Proof

Step Hyp Ref Expression
1 ralrexbid.1 φ ψ θ
2 df-ral x A φ x x A φ
3 1 imim2i x A φ x A ψ θ
4 3 pm5.32d x A φ x A ψ x A θ
5 4 alexbii x x A φ x x A ψ x x A θ
6 2 5 sylbi x A φ x x A ψ x x A θ
7 df-rex x A ψ x x A ψ
8 df-rex x A θ x x A θ
9 6 7 8 3bitr4g x A φ x A ψ x A θ