Theorem opeq12d 3870

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 3864	. 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 1397   <.cop 3672

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678

This theorem is referenced by:  nfopd  3879  moop2  4344  funopsn  5829  fliftfuns  5938  elxp6  6331  dfmpo  6387  tfrlemi1  6497  qliftfuns  6787  xpassen  7013  xpdom2  7014  xpf1o  7029  xpmapenlem  7034  xpmapen  7035  dfplpq2  7573  dfmpq2  7574  addpipqqs  7589  mulpipq2  7590  mulpipq  7591  mulpipqqs  7592  mulidnq  7608  addnq0mo  7666  mulnq0mo  7667  addnnnq0  7668  mulnnnq0  7669  nqnq0a  7673  nqnq0m  7674  nq0a0  7676  nq02m  7684  genpdf  7727  genipv  7728  genpelxp  7730  addcomprg  7797  mulcomprg  7799  prplnqu  7839  cauappcvgprlemlim  7880  caucvgprprlemell  7904  caucvgprprlemelu  7905  caucvgprprlemcbv  7906  caucvgprprlemval  7907  caucvgprprlemnkeqj  7909  caucvgprprlemml  7913  caucvgprprlemmu  7914  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemopu  7918  caucvgprprlemloc  7922  caucvgprprlemclphr  7924  caucvgprprlemexbt  7925  caucvgprprlem1  7928  caucvgprprlem2  7929  addsrmo  7962  mulsrmo  7963  addsrpr  7964  mulsrpr  7965  caucvgsr  8021  addcnsr  8053  mulcnsr  8054  mulresr  8057  pitonnlem2  8066  pitonn  8067  recidpipr  8075  axaddcom  8089  ax0id  8097  axcnre  8100  nntopi  8113  axcaucvglemval  8116  frecuzrdgrrn  10669  frec2uzrdg  10670  frecuzrdgrcl  10671  frecuzrdgsuc  10675  frecuzrdgrclt  10676  frecuzrdgg  10677  frecuzrdgsuctlem  10684  seqeq1  10711  iseqvalcbv  10720  seq3val  10721  seqvalcd  10722  pfxsuff1eqwrdeq  11279  swrdpfx  11287  ccatopth  11296  swrdccatin2d  11324  eucalgval2  12624  qnumdenbi  12763  crth  12795  phimullem  12796  ennnfonelemg  13023  ennnfonelem1  13027  ressval3d  13154  imasex  13387  imasival  13388  imasaddvallemg  13397  xpsff1o  13431  txcnp  14994  upxp  14995  uptx  14997  txlm  15002  cnmpt1t  15008  cnmpt2t  15016  txhmeo  15042  mpodvdsmulf1o  15713