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  10797  frec2uzrdg  10798  frecuzrdgrcl  10799  frecuzrdgsuc  10803  frecuzrdgrclt  10804  frecuzrdgg  10805  frecuzrdgsuctlem  10812  seqeq1  10839  iseqvalcbv  10848  seq3val  10849  seqvalcd  10850  pfxsuff1eqwrdeq  11419  swrdpfx  11427  ccatopth  11436  swrdccatin2d  11464  eucalgval2  12779  qnumdenbi  12918  crth  12950  phimullem  12951  ennnfonelemg  13242  ennnfonelem1  13246  ressval3d  13373  imasex  13573  imasival  13574  imasaddvallemg  13583  xpsff1o  13617  txcnp  15266  upxp  15267  uptx  15269  txlm  15274  cnmpt1t  15280  cnmpt2t  15288  txhmeo  15314  pellexlem3  15977  mpodvdsmulf1o  15988