Theorem opeq12d 3786

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 3780	. 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 1353   <.cop 3595

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601

This theorem is referenced by:  nfopd  3795  moop2  4251  fliftfuns  5798  elxp6  6169  dfmpo  6223  tfrlemi1  6332  qliftfuns  6618  xpassen  6829  xpdom2  6830  xpf1o  6843  xpmapenlem  6848  xpmapen  6849  dfplpq2  7352  dfmpq2  7353  addpipqqs  7368  mulpipq2  7369  mulpipq  7370  mulpipqqs  7371  mulidnq  7387  addnq0mo  7445  mulnq0mo  7446  addnnnq0  7447  mulnnnq0  7448  nqnq0a  7452  nqnq0m  7453  nq0a0  7455  nq02m  7463  genpdf  7506  genipv  7507  genpelxp  7509  addcomprg  7576  mulcomprg  7578  prplnqu  7618  cauappcvgprlemlim  7659  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemnkeqj  7688  caucvgprprlemml  7692  caucvgprprlemmu  7693  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemopu  7697  caucvgprprlemloc  7701  caucvgprprlemclphr  7703  caucvgprprlemexbt  7704  caucvgprprlem1  7707  caucvgprprlem2  7708  addsrmo  7741  mulsrmo  7742  addsrpr  7743  mulsrpr  7744  caucvgsr  7800  addcnsr  7832  mulcnsr  7833  mulresr  7836  pitonnlem2  7845  pitonn  7846  recidpipr  7854  axaddcom  7868  ax0id  7876  axcnre  7879  nntopi  7892  axcaucvglemval  7895  frecuzrdgrrn  10407  frec2uzrdg  10408  frecuzrdgrcl  10409  frecuzrdgsuc  10413  frecuzrdgrclt  10414  frecuzrdgg  10415  frecuzrdgsuctlem  10422  seqeq1  10447  iseqvalcbv  10456  seq3val  10457  seqvalcd  10458  eucalgval2  12052  qnumdenbi  12191  crth  12223  phimullem  12224  ennnfonelemg  12403  ennnfonelem1  12407  ressval3d  12530  imasex  12725  imasival  12726  imasaddvallemg  12735  xpsff1o  12767  txcnp  13741  upxp  13742  uptx  13744  txlm  13749  cnmpt1t  13755  cnmpt2t  13763  txhmeo  13789