Theorem opeq12d 3907

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

Syntax hints:   -> wi 4   = wceq 1402   <.cop 3708

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714

This theorem is referenced by:  nfopd  3916  moop2  4387  fsn2g  5874  funopsn  5882  fliftfuns  5994  elxp6  6393  dfmpo  6449  tfrlemi1  6593  qliftfuns  6883  xpassen  7118  xpdom2  7119  xpf1o  7134  xpmapenlem  7139  xpmapen  7140  mapunen  7141  dfplpq2  7711  dfmpq2  7712  addpipqqs  7727  mulpipq2  7728  mulpipq  7729  mulpipqqs  7730  mulidnq  7746  addnq0mo  7804  mulnq0mo  7805  addnnnq0  7806  mulnnnq0  7807  nqnq0a  7811  nqnq0m  7812  nq0a0  7814  nq02m  7822  genpdf  7865  genipv  7866  genpelxp  7868  addcomprg  7935  mulcomprg  7937  prplnqu  7977  cauappcvgprlemlim  8018  caucvgprprlemell  8042  caucvgprprlemelu  8043  caucvgprprlemcbv  8044  caucvgprprlemval  8045  caucvgprprlemnkeqj  8047  caucvgprprlemml  8051  caucvgprprlemmu  8052  caucvgprprlemopl  8054  caucvgprprlemlol  8055  caucvgprprlemopu  8056  caucvgprprlemloc  8060  caucvgprprlemclphr  8062  caucvgprprlemexbt  8063  caucvgprprlem1  8066  caucvgprprlem2  8067  addsrmo  8100  mulsrmo  8101  addsrpr  8102  mulsrpr  8103  caucvgsr  8159  addcnsr  8191  mulcnsr  8192  mulresr  8195  pitonnlem2  8204  pitonn  8205  recidpipr  8213  axaddcom  8227  ax0id  8235  axcnre  8238  nntopi  8251  axcaucvglemval  8254  frecuzrdgrrn  10823  frec2uzrdg  10824  frecuzrdgrcl  10825  frecuzrdgsuc  10829  frecuzrdgrclt  10830  frecuzrdgg  10831  frecuzrdgsuctlem  10838  seqeq1  10865  iseqvalcbv  10874  seq3val  10875  seqvalcd  10876  pfxsuff1eqwrdeq  11449  swrdpfx  11457  ccatopth  11466  swrdccatin2d  11494  eucalgval2  12809  qnumdenbi  12948  crth  12980  phimullem  12981  ennnfonelemg  13272  ennnfonelem1  13276  ressval3d  13403  imasex  13603  imasival  13604  imasaddvallemg  13613  xpsff1o  13647  txcnp  15295  upxp  15296  uptx  15298  txlm  15303  cnmpt1t  15309  cnmpt2t  15317  txhmeo  15343  pellexlem3  16007  mpodvdsmulf1o  16018