Theorem cleqan12d 1116

Description: A useful inference for substituting definitions into an equality.

Hypotheses

Ref	Expression
cleqan12d.1	|- (ph -> A = B)
cleqan12d.2	|- (ps -> C = D)

Assertion

Ref	Expression
cleqan12d	|- ((ph /\ ps) -> (A = C <-> B = D))

Proof of Theorem cleqan12d

Step	Hyp	Ref	Expression
1		cleqan12d.1	. . 3 |- (ph -> A = B)
2	1	adantr 306	. 2 |- ((ph /\ ps) -> A = B)
3		cleqan12d.2	. . 3 |- (ps -> C = D)
4	3	adantl 305	. 2 |- ((ph /\ ps) -> C = D)
5	2, 4	cleq12d 1115	1 |- ((ph /\ ps) -> (A = C <-> B = D))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196   = wceq 1091

This theorem is referenced by:  cleqan12rd 1117  opth2 1909  tz7.48lem 2993  ecopopreq 3244  xpdom2 3345  unfilem2 3439  suc11reg 3456  addpipq 3848  mulpipq 3849  addsrpr 3978  mulsrpr 3979  nnleltp1t 4448  zneo 4601  xpnnen 4927  znnen 4930  infmap2lem2 4952

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org