Theorem opeq12d 3870

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	⊢ (𝜑 → 𝐴 = 𝐵)
opeq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
opeq12d	⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)

Proof of Theorem opeq12d

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		opeq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		opeq12 3864	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)

Syntax hints:   → wi 4   = wceq 1397  ⟨cop 3672

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678

This theorem is referenced by:  nfopd  3879  moop2  4344  fsn2g  5822  funopsn  5830  fliftfuns  5939  elxp6  6332  dfmpo  6388  tfrlemi1  6498  qliftfuns  6788  xpassen  7014  xpdom2  7015  xpf1o  7030  xpmapenlem  7035  xpmapen  7036  dfplpq2  7574  dfmpq2  7575  addpipqqs  7590  mulpipq2  7591  mulpipq  7592  mulpipqqs  7593  mulidnq  7609  addnq0mo  7667  mulnq0mo  7668  addnnnq0  7669  mulnnnq0  7670  nqnq0a  7674  nqnq0m  7675  nq0a0  7677  nq02m  7685  genpdf  7728  genipv  7729  genpelxp  7731  addcomprg  7798  mulcomprg  7800  prplnqu  7840  cauappcvgprlemlim  7881  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemnkeqj  7910  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemloc  7923  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  caucvgprprlem1  7929  caucvgprprlem2  7930  addsrmo  7963  mulsrmo  7964  addsrpr  7965  mulsrpr  7966  caucvgsr  8022  addcnsr  8054  mulcnsr  8055  mulresr  8058  pitonnlem2  8067  pitonn  8068  recidpipr  8076  axaddcom  8090  ax0id  8098  axcnre  8101  nntopi  8114  axcaucvglemval  8117  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgg  10679  frecuzrdgsuctlem  10686  seqeq1  10713  iseqvalcbv  10722  seq3val  10723  seqvalcd  10724  pfxsuff1eqwrdeq  11284  swrdpfx  11292  ccatopth  11301  swrdccatin2d  11329  eucalgval2  12630  qnumdenbi  12769  crth  12801  phimullem  12802  ennnfonelemg  13029  ennnfonelem1  13033  ressval3d  13160  imasex  13393  imasival  13394  imasaddvallemg  13403  xpsff1o  13437  txcnp  15001  upxp  15002  uptx  15004  txlm  15009  cnmpt1t  15015  cnmpt2t  15023  txhmeo  15049  mpodvdsmulf1o  15720