Theorem opeq12d 3841

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 3835	. 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 3646

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652

This theorem is referenced by:  nfopd  3850  moop2  4314  funopsn  5785  fliftfuns  5890  elxp6  6278  dfmpo  6332  tfrlemi1  6441  qliftfuns  6729  xpassen  6950  xpdom2  6951  xpf1o  6966  xpmapenlem  6971  xpmapen  6972  dfplpq2  7502  dfmpq2  7503  addpipqqs  7518  mulpipq2  7519  mulpipq  7520  mulpipqqs  7521  mulidnq  7537  addnq0mo  7595  mulnq0mo  7596  addnnnq0  7597  mulnnnq0  7598  nqnq0a  7602  nqnq0m  7603  nq0a0  7605  nq02m  7613  genpdf  7656  genipv  7657  genpelxp  7659  addcomprg  7726  mulcomprg  7728  prplnqu  7768  cauappcvgprlemlim  7809  caucvgprprlemell  7833  caucvgprprlemelu  7834  caucvgprprlemcbv  7835  caucvgprprlemval  7836  caucvgprprlemnkeqj  7838  caucvgprprlemml  7842  caucvgprprlemmu  7843  caucvgprprlemopl  7845  caucvgprprlemlol  7846  caucvgprprlemopu  7847  caucvgprprlemloc  7851  caucvgprprlemclphr  7853  caucvgprprlemexbt  7854  caucvgprprlem1  7857  caucvgprprlem2  7858  addsrmo  7891  mulsrmo  7892  addsrpr  7893  mulsrpr  7894  caucvgsr  7950  addcnsr  7982  mulcnsr  7983  mulresr  7986  pitonnlem2  7995  pitonn  7996  recidpipr  8004  axaddcom  8018  ax0id  8026  axcnre  8029  nntopi  8042  axcaucvglemval  8045  frecuzrdgrrn  10590  frec2uzrdg  10591  frecuzrdgrcl  10592  frecuzrdgsuc  10596  frecuzrdgrclt  10597  frecuzrdgg  10598  frecuzrdgsuctlem  10605  seqeq1  10632  iseqvalcbv  10641  seq3val  10642  seqvalcd  10643  pfxsuff1eqwrdeq  11190  swrdpfx  11198  ccatopth  11207  swrdccatin2d  11235  eucalgval2  12490  qnumdenbi  12629  crth  12661  phimullem  12662  ennnfonelemg  12889  ennnfonelem1  12893  ressval3d  13019  imasex  13252  imasival  13253  imasaddvallemg  13262  xpsff1o  13296  txcnp  14858  upxp  14859  uptx  14861  txlm  14866  cnmpt1t  14872  cnmpt2t  14880  txhmeo  14906  mpodvdsmulf1o  15577