Theorem opeq12d 3801

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 3795	. 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 1364   <.cop 3610

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616

This theorem is referenced by:  nfopd  3810  moop2  4269  fliftfuns  5820  elxp6  6195  dfmpo  6249  tfrlemi1  6358  qliftfuns  6646  xpassen  6857  xpdom2  6858  xpf1o  6873  xpmapenlem  6878  xpmapen  6879  dfplpq2  7384  dfmpq2  7385  addpipqqs  7400  mulpipq2  7401  mulpipq  7402  mulpipqqs  7403  mulidnq  7419  addnq0mo  7477  mulnq0mo  7478  addnnnq0  7479  mulnnnq0  7480  nqnq0a  7484  nqnq0m  7485  nq0a0  7487  nq02m  7495  genpdf  7538  genipv  7539  genpelxp  7541  addcomprg  7608  mulcomprg  7610  prplnqu  7650  cauappcvgprlemlim  7691  caucvgprprlemell  7715  caucvgprprlemelu  7716  caucvgprprlemcbv  7717  caucvgprprlemval  7718  caucvgprprlemnkeqj  7720  caucvgprprlemml  7724  caucvgprprlemmu  7725  caucvgprprlemopl  7727  caucvgprprlemlol  7728  caucvgprprlemopu  7729  caucvgprprlemloc  7733  caucvgprprlemclphr  7735  caucvgprprlemexbt  7736  caucvgprprlem1  7739  caucvgprprlem2  7740  addsrmo  7773  mulsrmo  7774  addsrpr  7775  mulsrpr  7776  caucvgsr  7832  addcnsr  7864  mulcnsr  7865  mulresr  7868  pitonnlem2  7877  pitonn  7878  recidpipr  7886  axaddcom  7900  ax0id  7908  axcnre  7911  nntopi  7924  axcaucvglemval  7927  frecuzrdgrrn  10441  frec2uzrdg  10442  frecuzrdgrcl  10443  frecuzrdgsuc  10447  frecuzrdgrclt  10448  frecuzrdgg  10449  frecuzrdgsuctlem  10456  seqeq1  10481  iseqvalcbv  10490  seq3val  10491  seqvalcd  10492  eucalgval2  12088  qnumdenbi  12227  crth  12259  phimullem  12260  ennnfonelemg  12457  ennnfonelem1  12461  ressval3d  12587  imasex  12785  imasival  12786  imasaddvallemg  12795  xpsff1o  12828  txcnp  14248  upxp  14249  uptx  14251  txlm  14256  cnmpt1t  14262  cnmpt2t  14270  txhmeo  14296