Theorem opeq12d 3557

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 3551	. 2 |- ( ( A = B /\ C = D ) -> <. A , C >. = <. B , D >. )
4	1, 2, 3	syl2anc 391	1 |- ( ph -> <. A , C >. = <. B , D >. )

Syntax hints:   -> wi 4   = wceq 1243   <.cop 3378

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384

This theorem is referenced by:  nfopd  3566  moop2  3988  fliftfuns  5438  elxp6  5796  dfmpt2  5844  tfrlemi1  5946  qliftfuns  6190  xpassen  6304  xpdom2  6305  dfplpq2  6452  dfmpq2  6453  addpipqqs  6468  mulpipq2  6469  mulpipq  6470  mulpipqqs  6471  mulidnq  6487  addnq0mo  6545  mulnq0mo  6546  addnnnq0  6547  mulnnnq0  6548  nqnq0a  6552  nqnq0m  6553  nq0a0  6555  nq02m  6563  genpdf  6606  genipv  6607  genpelxp  6609  addcomprg  6676  mulcomprg  6678  prplnqu  6718  cauappcvgprlemlim  6759  caucvgprprlemell  6783  caucvgprprlemelu  6784  caucvgprprlemcbv  6785  caucvgprprlemval  6786  caucvgprprlemnkeqj  6788  caucvgprprlemml  6792  caucvgprprlemmu  6793  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemopu  6797  caucvgprprlemloc  6801  caucvgprprlemclphr  6803  caucvgprprlemexbt  6804  caucvgprprlem1  6807  caucvgprprlem2  6808  addsrmo  6828  mulsrmo  6829  addsrpr  6830  mulsrpr  6831  caucvgsr  6886  addcnsr  6910  mulcnsr  6911  mulresr  6914  pitonnlem2  6923  pitonn  6924  recidpipr  6932  axaddcom  6944  ax0id  6952  axcnre  6955  nntopi  6968  axcaucvglemval  6971  frecuzrdgrrn  9194  frec2uzrdg  9195  frecuzrdgsuc  9201  iseqeq1  9214