Theorem opeq12d 3896

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 3890	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)

Syntax hints:   → wi 4   = wceq 1398  ⟨cop 3697

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703

This theorem is referenced by:  nfopd  3905  moop2  4373  fsn2g  5857  funopsn  5865  fliftfuns  5977  elxp6  6376  dfmpo  6432  tfrlemi1  6576  qliftfuns  6866  xpassen  7094  xpdom2  7095  xpf1o  7110  xpmapenlem  7115  xpmapen  7116  mapunen  7117  dfplpq2  7685  dfmpq2  7686  addpipqqs  7701  mulpipq2  7702  mulpipq  7703  mulpipqqs  7704  mulidnq  7720  addnq0mo  7778  mulnq0mo  7779  addnnnq0  7780  mulnnnq0  7781  nqnq0a  7785  nqnq0m  7786  nq0a0  7788  nq02m  7796  genpdf  7839  genipv  7840  genpelxp  7842  addcomprg  7909  mulcomprg  7911  prplnqu  7951  cauappcvgprlemlim  7992  caucvgprprlemell  8016  caucvgprprlemelu  8017  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemnkeqj  8021  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemloc  8034  caucvgprprlemclphr  8036  caucvgprprlemexbt  8037  caucvgprprlem1  8040  caucvgprprlem2  8041  addsrmo  8074  mulsrmo  8075  addsrpr  8076  mulsrpr  8077  caucvgsr  8133  addcnsr  8165  mulcnsr  8166  mulresr  8169  pitonnlem2  8178  pitonn  8179  recidpipr  8187  axaddcom  8201  ax0id  8209  axcnre  8212  nntopi  8225  axcaucvglemval  8228  frecuzrdgrrn  10794  frec2uzrdg  10795  frecuzrdgrcl  10796  frecuzrdgsuc  10800  frecuzrdgrclt  10801  frecuzrdgg  10802  frecuzrdgsuctlem  10809  seqeq1  10836  iseqvalcbv  10845  seq3val  10846  seqvalcd  10847  pfxsuff1eqwrdeq  11416  swrdpfx  11424  ccatopth  11433  swrdccatin2d  11461  eucalgval2  12775  qnumdenbi  12914  crth  12946  phimullem  12947  ennnfonelemg  13238  ennnfonelem1  13242  ressval3d  13369  imasex  13602  imasival  13603  imasaddvallemg  13612  xpsff1o  13646  txcnp  15248  upxp  15249  uptx  15251  txlm  15256  cnmpt1t  15262  cnmpt2t  15270  txhmeo  15296  pellexlem3  15959  mpodvdsmulf1o  15970