Metamath Proof Explorer


Theorem subtr

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

Ref Expression
Hypotheses subtr.1 _xA
subtr.2 _xB
subtr.3 _xY
subtr.4 _xZ
subtr.5 x=AX=Y
subtr.6 x=BX=Z
Assertion subtr ACBDA=BY=Z

Proof

Step Hyp Ref Expression
1 subtr.1 _xA
2 subtr.2 _xB
3 subtr.3 _xY
4 subtr.4 _xZ
5 subtr.5 x=AX=Y
6 subtr.6 x=BX=Z
7 1 2 nfeq xA=B
8 3 4 nfeq xY=Z
9 7 8 nfim xA=BY=Z
10 eqeq1 x=Ax=BA=B
11 5 eqeq1d x=AX=ZY=Z
12 10 11 imbi12d x=Ax=BX=ZA=BY=Z
13 1 9 12 6 vtoclgf ACA=BY=Z
14 13 adantr ACBDA=BY=Z