Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT . (Contributed by NM, 9Aug1994) (Proof shortened by Andrew Salmon, 25May2011) (Proof shortened by Wolf Lammen, 20Nov2019)
Ref  Expression  

Hypotheses  eqeqan12d.1   ( ph > A = B ) 

eqeqan12d.2   ( ps > C = D ) 

Assertion  eqeqan12d   ( ( ph /\ ps ) > ( A = C <> B = D ) ) 
Step  Hyp  Ref  Expression 

1  eqeqan12d.1   ( ph > A = B ) 

2  eqeqan12d.2   ( ps > C = D ) 

3  1  adantr   ( ( ph /\ ps ) > A = B ) 
4  2  adantl   ( ( ph /\ ps ) > C = D ) 
5  3 4  eqeq12d   ( ( ph /\ ps ) > ( A = C <> B = D ) ) 