Theorem opeq12d 3812

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 3806	. 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 1364   <.cop 3621

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627

This theorem is referenced by:  nfopd  3821  moop2  4280  fliftfuns  5841  elxp6  6222  dfmpo  6276  tfrlemi1  6385  qliftfuns  6673  xpassen  6884  xpdom2  6885  xpf1o  6900  xpmapenlem  6905  xpmapen  6906  dfplpq2  7414  dfmpq2  7415  addpipqqs  7430  mulpipq2  7431  mulpipq  7432  mulpipqqs  7433  mulidnq  7449  addnq0mo  7507  mulnq0mo  7508  addnnnq0  7509  mulnnnq0  7510  nqnq0a  7514  nqnq0m  7515  nq0a0  7517  nq02m  7525  genpdf  7568  genipv  7569  genpelxp  7571  addcomprg  7638  mulcomprg  7640  prplnqu  7680  cauappcvgprlemlim  7721  caucvgprprlemell  7745  caucvgprprlemelu  7746  caucvgprprlemcbv  7747  caucvgprprlemval  7748  caucvgprprlemnkeqj  7750  caucvgprprlemml  7754  caucvgprprlemmu  7755  caucvgprprlemopl  7757  caucvgprprlemlol  7758  caucvgprprlemopu  7759  caucvgprprlemloc  7763  caucvgprprlemclphr  7765  caucvgprprlemexbt  7766  caucvgprprlem1  7769  caucvgprprlem2  7770  addsrmo  7803  mulsrmo  7804  addsrpr  7805  mulsrpr  7806  caucvgsr  7862  addcnsr  7894  mulcnsr  7895  mulresr  7898  pitonnlem2  7907  pitonn  7908  recidpipr  7916  axaddcom  7930  ax0id  7938  axcnre  7941  nntopi  7954  axcaucvglemval  7957  frecuzrdgrrn  10479  frec2uzrdg  10480  frecuzrdgrcl  10481  frecuzrdgsuc  10485  frecuzrdgrclt  10486  frecuzrdgg  10487  frecuzrdgsuctlem  10494  seqeq1  10521  iseqvalcbv  10530  seq3val  10531  seqvalcd  10532  eucalgval2  12191  qnumdenbi  12330  crth  12362  phimullem  12363  ennnfonelemg  12560  ennnfonelem1  12564  ressval3d  12690  imasex  12888  imasival  12889  imasaddvallemg  12898  xpsff1o  12932  txcnp  14439  upxp  14440  uptx  14442  txlm  14447  cnmpt1t  14453  cnmpt2t  14461  txhmeo  14487