Theorem opeq12d 3865

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 3859	. 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 1395   <.cop 3669

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675

This theorem is referenced by:  nfopd  3874  moop2  4338  funopsn  5819  fliftfuns  5928  elxp6  6321  dfmpo  6375  tfrlemi1  6484  qliftfuns  6774  xpassen  6997  xpdom2  6998  xpf1o  7013  xpmapenlem  7018  xpmapen  7019  dfplpq2  7552  dfmpq2  7553  addpipqqs  7568  mulpipq2  7569  mulpipq  7570  mulpipqqs  7571  mulidnq  7587  addnq0mo  7645  mulnq0mo  7646  addnnnq0  7647  mulnnnq0  7648  nqnq0a  7652  nqnq0m  7653  nq0a0  7655  nq02m  7663  genpdf  7706  genipv  7707  genpelxp  7709  addcomprg  7776  mulcomprg  7778  prplnqu  7818  cauappcvgprlemlim  7859  caucvgprprlemell  7883  caucvgprprlemelu  7884  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemnkeqj  7888  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemopu  7897  caucvgprprlemloc  7901  caucvgprprlemclphr  7903  caucvgprprlemexbt  7904  caucvgprprlem1  7907  caucvgprprlem2  7908  addsrmo  7941  mulsrmo  7942  addsrpr  7943  mulsrpr  7944  caucvgsr  8000  addcnsr  8032  mulcnsr  8033  mulresr  8036  pitonnlem2  8045  pitonn  8046  recidpipr  8054  axaddcom  8068  ax0id  8076  axcnre  8079  nntopi  8092  axcaucvglemval  8095  frecuzrdgrrn  10642  frec2uzrdg  10643  frecuzrdgrcl  10644  frecuzrdgsuc  10648  frecuzrdgrclt  10649  frecuzrdgg  10650  frecuzrdgsuctlem  10657  seqeq1  10684  iseqvalcbv  10693  seq3val  10694  seqvalcd  10695  pfxsuff1eqwrdeq  11246  swrdpfx  11254  ccatopth  11263  swrdccatin2d  11291  eucalgval2  12590  qnumdenbi  12729  crth  12761  phimullem  12762  ennnfonelemg  12989  ennnfonelem1  12993  ressval3d  13120  imasex  13353  imasival  13354  imasaddvallemg  13363  xpsff1o  13397  txcnp  14960  upxp  14961  uptx  14963  txlm  14968  cnmpt1t  14974  cnmpt2t  14982  txhmeo  15008  mpodvdsmulf1o  15679