Theorem opeq12d 3713

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

Syntax hints:   -> wi 4   = wceq 1331   <.cop 3530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536

This theorem is referenced by:  nfopd  3722  moop2  4173  fliftfuns  5699  elxp6  6067  dfmpo  6120  tfrlemi1  6229  qliftfuns  6513  xpassen  6724  xpdom2  6725  xpf1o  6738  xpmapenlem  6743  xpmapen  6744  dfplpq2  7169  dfmpq2  7170  addpipqqs  7185  mulpipq2  7186  mulpipq  7187  mulpipqqs  7188  mulidnq  7204  addnq0mo  7262  mulnq0mo  7263  addnnnq0  7264  mulnnnq0  7265  nqnq0a  7269  nqnq0m  7270  nq0a0  7272  nq02m  7280  genpdf  7323  genipv  7324  genpelxp  7326  addcomprg  7393  mulcomprg  7395  prplnqu  7435  cauappcvgprlemlim  7476  caucvgprprlemell  7500  caucvgprprlemelu  7501  caucvgprprlemcbv  7502  caucvgprprlemval  7503  caucvgprprlemnkeqj  7505  caucvgprprlemml  7509  caucvgprprlemmu  7510  caucvgprprlemopl  7512  caucvgprprlemlol  7513  caucvgprprlemopu  7514  caucvgprprlemloc  7518  caucvgprprlemclphr  7520  caucvgprprlemexbt  7521  caucvgprprlem1  7524  caucvgprprlem2  7525  addsrmo  7558  mulsrmo  7559  addsrpr  7560  mulsrpr  7561  caucvgsr  7617  addcnsr  7649  mulcnsr  7650  mulresr  7653  pitonnlem2  7662  pitonn  7663  recidpipr  7671  axaddcom  7685  ax0id  7693  axcnre  7696  nntopi  7709  axcaucvglemval  7712  frecuzrdgrrn  10188  frec2uzrdg  10189  frecuzrdgrcl  10190  frecuzrdgsuc  10194  frecuzrdgrclt  10195  frecuzrdgg  10196  frecuzrdgsuctlem  10203  seqeq1  10228  iseqvalcbv  10237  seq3val  10238  seqvalcd  10239  eucalgval2  11741  qnumdenbi  11877  crth  11907  phimullem  11908  ennnfonelemg  11923  ennnfonelem1  11927  txcnp  12450  upxp  12451  uptx  12453  txlm  12458  cnmpt1t  12464  cnmpt2t  12472  txhmeo  12498