Theorem opeq12d 3827

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 3821	. 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 1373   <.cop 3636

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642

This theorem is referenced by:  nfopd  3836  moop2  4296  funopsn  5762  fliftfuns  5867  elxp6  6255  dfmpo  6309  tfrlemi1  6418  qliftfuns  6706  xpassen  6925  xpdom2  6926  xpf1o  6941  xpmapenlem  6946  xpmapen  6947  dfplpq2  7467  dfmpq2  7468  addpipqqs  7483  mulpipq2  7484  mulpipq  7485  mulpipqqs  7486  mulidnq  7502  addnq0mo  7560  mulnq0mo  7561  addnnnq0  7562  mulnnnq0  7563  nqnq0a  7567  nqnq0m  7568  nq0a0  7570  nq02m  7578  genpdf  7621  genipv  7622  genpelxp  7624  addcomprg  7691  mulcomprg  7693  prplnqu  7733  cauappcvgprlemlim  7774  caucvgprprlemell  7798  caucvgprprlemelu  7799  caucvgprprlemcbv  7800  caucvgprprlemval  7801  caucvgprprlemnkeqj  7803  caucvgprprlemml  7807  caucvgprprlemmu  7808  caucvgprprlemopl  7810  caucvgprprlemlol  7811  caucvgprprlemopu  7812  caucvgprprlemloc  7816  caucvgprprlemclphr  7818  caucvgprprlemexbt  7819  caucvgprprlem1  7822  caucvgprprlem2  7823  addsrmo  7856  mulsrmo  7857  addsrpr  7858  mulsrpr  7859  caucvgsr  7915  addcnsr  7947  mulcnsr  7948  mulresr  7951  pitonnlem2  7960  pitonn  7961  recidpipr  7969  axaddcom  7983  ax0id  7991  axcnre  7994  nntopi  8007  axcaucvglemval  8010  frecuzrdgrrn  10553  frec2uzrdg  10554  frecuzrdgrcl  10555  frecuzrdgsuc  10559  frecuzrdgrclt  10560  frecuzrdgg  10561  frecuzrdgsuctlem  10568  seqeq1  10595  iseqvalcbv  10604  seq3val  10605  seqvalcd  10606  eucalgval2  12375  qnumdenbi  12514  crth  12546  phimullem  12547  ennnfonelemg  12774  ennnfonelem1  12778  ressval3d  12904  imasex  13137  imasival  13138  imasaddvallemg  13147  xpsff1o  13181  txcnp  14743  upxp  14744  uptx  14746  txlm  14751  cnmpt1t  14757  cnmpt2t  14765  txhmeo  14791  mpodvdsmulf1o  15462