Theorem opeq12d 3721

Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Hypotheses

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

Assertion

Ref	Expression
opeq12d	|- ( ph -> <. A , C >. = <. B , D >. )

Proof of Theorem opeq12d

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 |- ( ph -> A = B )
2		opeq12d.2	. 2 |- ( ph -> C = D )
3		opeq12 3715	. 2 |- ( ( A = B /\ C = D ) -> <. A , C >. = <. B , D >. )
4	1, 2, 3	syl2anc 409	1 |- ( ph -> <. A , C >. = <. B , D >. )

Syntax hints:   -> wi 4   = wceq 1332   <.cop 3535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541

This theorem is referenced by:  nfopd  3730  moop2  4181  fliftfuns  5707  elxp6  6075  dfmpo  6128  tfrlemi1  6237  qliftfuns  6521  xpassen  6732  xpdom2  6733  xpf1o  6746  xpmapenlem  6751  xpmapen  6752  dfplpq2  7186  dfmpq2  7187  addpipqqs  7202  mulpipq2  7203  mulpipq  7204  mulpipqqs  7205  mulidnq  7221  addnq0mo  7279  mulnq0mo  7280  addnnnq0  7281  mulnnnq0  7282  nqnq0a  7286  nqnq0m  7287  nq0a0  7289  nq02m  7297  genpdf  7340  genipv  7341  genpelxp  7343  addcomprg  7410  mulcomprg  7412  prplnqu  7452  cauappcvgprlemlim  7493  caucvgprprlemell  7517  caucvgprprlemelu  7518  caucvgprprlemcbv  7519  caucvgprprlemval  7520  caucvgprprlemnkeqj  7522  caucvgprprlemml  7526  caucvgprprlemmu  7527  caucvgprprlemopl  7529  caucvgprprlemlol  7530  caucvgprprlemopu  7531  caucvgprprlemloc  7535  caucvgprprlemclphr  7537  caucvgprprlemexbt  7538  caucvgprprlem1  7541  caucvgprprlem2  7542  addsrmo  7575  mulsrmo  7576  addsrpr  7577  mulsrpr  7578  caucvgsr  7634  addcnsr  7666  mulcnsr  7667  mulresr  7670  pitonnlem2  7679  pitonn  7680  recidpipr  7688  axaddcom  7702  ax0id  7710  axcnre  7713  nntopi  7726  axcaucvglemval  7729  frecuzrdgrrn  10212  frec2uzrdg  10213  frecuzrdgrcl  10214  frecuzrdgsuc  10218  frecuzrdgrclt  10219  frecuzrdgg  10220  frecuzrdgsuctlem  10227  seqeq1  10252  iseqvalcbv  10261  seq3val  10262  seqvalcd  10263  eucalgval2  11770  qnumdenbi  11906  crth  11936  phimullem  11937  ennnfonelemg  11952  ennnfonelem1  11956  txcnp  12479  upxp  12480  uptx  12482  txlm  12487  cnmpt1t  12493  cnmpt2t  12501  txhmeo  12527