Theorem wl-dral1d 33318

Description: A version of dral1 2325 with a context. Note: At first glance one might be tempted to generalize this (or a similar) theorem by weakening the first two hypotheses adding a x = y, A. x x = y or ph antecedent. wl-equsal1i 33329 and nf5di 2119 show that this is in fact pointless. (Contributed by Wolf Lammen, 28-Jul-2019.)

Hypotheses

Ref	Expression
wl-dral1d.1	|- F/ x ph
wl-dral1d.2	|- F/ y ph
wl-dral1d.3	|- ( ph -> ( x = y -> ( ps <-> ch ) ) )

Assertion

Ref	Expression
wl-dral1d	|- ( ph -> ( A. x x = y -> ( A. x ps <-> A. y ch ) ) )

Proof of Theorem wl-dral1d

Step	Hyp	Ref	Expression
1		wl-dral1d.3	. . . . . . . 8 |- ( ph -> ( x = y -> ( ps <-> ch ) ) )
2	1	com12 32	. . . . . . 7 |- ( x = y -> ( ph -> ( ps <-> ch ) ) )
3	2	pm5.74d 262	. . . . . 6 |- ( x = y -> ( ( ph -> ps ) <-> ( ph -> ch ) ) )
4	3	sps 2055	. . . . 5 |- ( A. x x = y -> ( ( ph -> ps ) <-> ( ph -> ch ) ) )
5	4	dral1 2325	. . . 4 |- ( A. x x = y -> ( A. x ( ph -> ps ) <-> A. y ( ph -> ch ) ) )
6		wl-dral1d.1	. . . . 5 |- F/ x ph
7	6	19.21 2075	. . . 4 |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )
8		wl-dral1d.2	. . . . 5 |- F/ y ph
9	8	19.21 2075	. . . 4 |- ( A. y ( ph -> ch ) <-> ( ph -> A. y ch ) )
10	5, 7, 9	3bitr3g 302	. . 3 |- ( A. x x = y -> ( ( ph -> A. x ps ) <-> ( ph -> A. y ch ) ) )
11	10	pm5.74rd 263	. 2 |- ( A. x x = y -> ( ph -> ( A. x ps <-> A. y ch ) ) )
12	11	com12 32	1 |- ( ph -> ( A. x x = y -> ( A. x ps <-> A. y ch ) ) )

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710

This theorem is referenced by:  wl-cbvalnaed  33319