Theorem subtr2

Description: Transitivity of implicit substitution into a wff. (Contributed by Jeff Hankins, 19-Sep-2009) (Proof shortened by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Hypotheses	subtr.1	|- F/_ x A
	subtr.2	|- F/_ x B
	subtr2.3	|- F/ x ps
	subtr2.4	|- F/ x ch
	subtr2.5	|- ( x = A -> ( ph <-> ps ) )
	subtr2.6	|- ( x = B -> ( ph <-> ch ) )
Assertion	subtr2	|- ( ( A e. C /\ B e. D ) -> ( A = B -> ( ps <-> ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		subtr.1	|- F/_ x A
2		subtr.2	|- F/_ x B
3		subtr2.3	|- F/ x ps
4		subtr2.4	|- F/ x ch
5		subtr2.5	|- ( x = A -> ( ph <-> ps ) )
6		subtr2.6	|- ( x = B -> ( ph <-> ch ) )
7	1 2	nfeq	|- F/ x A = B
8	3 4	nfbi	|- F/ x ( ps <-> ch )
9	7 8	nfim	|- F/ x ( A = B -> ( ps <-> ch ) )
10		eqeq1	|- ( x = A -> ( x = B <-> A = B ) )
11	5	bibi1d	|- ( x = A -> ( ( ph <-> ch ) <-> ( ps <-> ch ) ) )
12	10 11	imbi12d	|- ( x = A -> ( ( x = B -> ( ph <-> ch ) ) <-> ( A = B -> ( ps <-> ch ) ) ) )
13	1 9 12 6	vtoclgf	|- ( A e. C -> ( A = B -> ( ps <-> ch ) ) )
14	13	adantr	|- ( ( A e. C /\ B e. D ) -> ( A = B -> ( ps <-> ch ) ) )