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-bnd 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  6429  mulnq0mo  6430  addnnnq0  6431  mulnnnq0  6432  nqnq0a  6436  nqnq0m  6437  nq0a0  6439  nq02m  6447  genpdf  6490  genipv  6491  genpelxp  6493  genpelpw  6499  addcomprg  6552  mulcomprg  6554  addsrmo  6631  mulsrmo  6632  addsrpr  6633  mulsrpr  6634  addcnsr  6691  mulcnsr  6692  mulresr  6695  pitonnlem2  6703  pitonn  6704  axaddcom  6714  ax0id  6722  axcnre  6725  frecuzrdgrrn  8835  frec2uzrdg  8836  frecuzrdgsuc  8842  iseqeq1  8854