Metamath Proof Explorer


Theorem ralbidar

Description: More general form of ralbida . (Contributed by Andrew Salmon, 25-Jul-2011)

Ref Expression
Hypotheses ralbidar.1 φ x A φ
ralbidar.2 φ x A ψ χ
Assertion ralbidar φ x A ψ x A χ

Proof

Step Hyp Ref Expression
1 ralbidar.1 φ x A φ
2 ralbidar.2 φ x A ψ χ
3 2 ex φ x A ψ χ
4 3 ralimi x A φ x A x A ψ χ
5 1 4 syl φ x A x A ψ χ
6 df-ral x A x A ψ χ x x A x A ψ χ
7 5 6 sylib φ x x A x A ψ χ
8 pm2.43 x A x A ψ χ x A ψ χ
9 8 pm5.74d x A x A ψ χ x A ψ x A χ
10 9 alimi x x A x A ψ χ x x A ψ x A χ
11 albi x x A ψ x A χ x x A ψ x x A χ
12 7 10 11 3syl φ x x A ψ x x A χ
13 df-ral x A ψ x x A ψ
14 df-ral x A χ x x A χ
15 12 13 14 3bitr4g φ x A ψ x A χ