Theorem opeq12d 3548

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 3542	. 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 1242   <.cop 3370

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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376

This theorem is referenced by:  nfopd  3557  moop2  3979  fliftfuns  5381  elxp6  5738  dfmpt2  5786  tfrlemi1  5887  qliftfuns  6126  xpassen  6240  xpdom2  6241  dfplpq2  6338  dfmpq2  6339  addpipqqs  6354  mulpipq2  6355  mulpipq  6356  mulpipqqs  6357  mulidnq  6373  addnq0mo  6430  mulnq0mo  6431  addnnnq0  6432  mulnnnq0  6433  nqnq0a  6437  nqnq0m  6438  nq0a0  6440  nq02m  6448  genpdf  6491  genipv  6492  genpelxp  6494  addcomprg  6554  mulcomprg  6556  cauappcvgprlemlim  6633  addsrmo  6671  mulsrmo  6672  addsrpr  6673  mulsrpr  6674  addcnsr  6731  mulcnsr  6732  mulresr  6735  pitonnlem2  6743  pitonn  6744  axaddcom  6754  ax0id  6762  axcnre  6765  frecuzrdgrrn  8875  frec2uzrdg  8876  frecuzrdgsuc  8882  iseqeq1  8894