Theorem opeq12d 3826

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 3820	. 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 1372   <.cop 3635

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641

This theorem is referenced by:  nfopd  3835  moop2  4295  funopsn  5761  fliftfuns  5866  elxp6  6254  dfmpo  6308  tfrlemi1  6417  qliftfuns  6705  xpassen  6924  xpdom2  6925  xpf1o  6940  xpmapenlem  6945  xpmapen  6946  dfplpq2  7466  dfmpq2  7467  addpipqqs  7482  mulpipq2  7483  mulpipq  7484  mulpipqqs  7485  mulidnq  7501  addnq0mo  7559  mulnq0mo  7560  addnnnq0  7561  mulnnnq0  7562  nqnq0a  7566  nqnq0m  7567  nq0a0  7569  nq02m  7577  genpdf  7620  genipv  7621  genpelxp  7623  addcomprg  7690  mulcomprg  7692  prplnqu  7732  cauappcvgprlemlim  7773  caucvgprprlemell  7797  caucvgprprlemelu  7798  caucvgprprlemcbv  7799  caucvgprprlemval  7800  caucvgprprlemnkeqj  7802  caucvgprprlemml  7806  caucvgprprlemmu  7807  caucvgprprlemopl  7809  caucvgprprlemlol  7810  caucvgprprlemopu  7811  caucvgprprlemloc  7815  caucvgprprlemclphr  7817  caucvgprprlemexbt  7818  caucvgprprlem1  7821  caucvgprprlem2  7822  addsrmo  7855  mulsrmo  7856  addsrpr  7857  mulsrpr  7858  caucvgsr  7914  addcnsr  7946  mulcnsr  7947  mulresr  7950  pitonnlem2  7959  pitonn  7960  recidpipr  7968  axaddcom  7982  ax0id  7990  axcnre  7993  nntopi  8006  axcaucvglemval  8009  frecuzrdgrrn  10551  frec2uzrdg  10552  frecuzrdgrcl  10553  frecuzrdgsuc  10557  frecuzrdgrclt  10558  frecuzrdgg  10559  frecuzrdgsuctlem  10566  seqeq1  10593  iseqvalcbv  10602  seq3val  10603  seqvalcd  10604  eucalgval2  12346  qnumdenbi  12485  crth  12517  phimullem  12518  ennnfonelemg  12745  ennnfonelem1  12749  ressval3d  12875  imasex  13108  imasival  13109  imasaddvallemg  13118  xpsff1o  13152  txcnp  14714  upxp  14715  uptx  14717  txlm  14722  cnmpt1t  14728  cnmpt2t  14736  txhmeo  14762  mpodvdsmulf1o  15433