Theorem opeq12d 3864

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 3858	. 2 |- ( ( A = B /\ C = D ) -> <. A , C >. = <. B , D >. )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> <. A , C >. = <. B , D >. )

Syntax hints:   -> wi 4   = wceq 1395   <.cop 3669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675

This theorem is referenced by:  nfopd  3873  moop2  4337  funopsn  5816  fliftfuns  5921  elxp6  6313  dfmpo  6367  tfrlemi1  6476  qliftfuns  6764  xpassen  6985  xpdom2  6986  xpf1o  7001  xpmapenlem  7006  xpmapen  7007  dfplpq2  7537  dfmpq2  7538  addpipqqs  7553  mulpipq2  7554  mulpipq  7555  mulpipqqs  7556  mulidnq  7572  addnq0mo  7630  mulnq0mo  7631  addnnnq0  7632  mulnnnq0  7633  nqnq0a  7637  nqnq0m  7638  nq0a0  7640  nq02m  7648  genpdf  7691  genipv  7692  genpelxp  7694  addcomprg  7761  mulcomprg  7763  prplnqu  7803  cauappcvgprlemlim  7844  caucvgprprlemell  7868  caucvgprprlemelu  7869  caucvgprprlemcbv  7870  caucvgprprlemval  7871  caucvgprprlemnkeqj  7873  caucvgprprlemml  7877  caucvgprprlemmu  7878  caucvgprprlemopl  7880  caucvgprprlemlol  7881  caucvgprprlemopu  7882  caucvgprprlemloc  7886  caucvgprprlemclphr  7888  caucvgprprlemexbt  7889  caucvgprprlem1  7892  caucvgprprlem2  7893  addsrmo  7926  mulsrmo  7927  addsrpr  7928  mulsrpr  7929  caucvgsr  7985  addcnsr  8017  mulcnsr  8018  mulresr  8021  pitonnlem2  8030  pitonn  8031  recidpipr  8039  axaddcom  8053  ax0id  8061  axcnre  8064  nntopi  8077  axcaucvglemval  8080  frecuzrdgrrn  10625  frec2uzrdg  10626  frecuzrdgrcl  10627  frecuzrdgsuc  10631  frecuzrdgrclt  10632  frecuzrdgg  10633  frecuzrdgsuctlem  10640  seqeq1  10667  iseqvalcbv  10676  seq3val  10677  seqvalcd  10678  pfxsuff1eqwrdeq  11226  swrdpfx  11234  ccatopth  11243  swrdccatin2d  11271  eucalgval2  12570  qnumdenbi  12709  crth  12741  phimullem  12742  ennnfonelemg  12969  ennnfonelem1  12973  ressval3d  13100  imasex  13333  imasival  13334  imasaddvallemg  13343  xpsff1o  13377  txcnp  14939  upxp  14940  uptx  14942  txlm  14947  cnmpt1t  14953  cnmpt2t  14961  txhmeo  14987  mpodvdsmulf1o  15658