Theorem opeq12d 3890

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-un 3214  df-sn 3694  df-pr 3695  df-op 3697

This theorem is referenced by:  nfopd  3899  moop2  4367  fsn2g  5851  funopsn  5859  fliftfuns  5970  elxp6  6362  dfmpo  6418  tfrlemi1  6562  qliftfuns  6852  xpassen  7080  xpdom2  7081  xpf1o  7096  xpmapenlem  7101  xpmapen  7102  mapunen  7103  dfplpq2  7668  dfmpq2  7669  addpipqqs  7684  mulpipq2  7685  mulpipq  7686  mulpipqqs  7687  mulidnq  7703  addnq0mo  7761  mulnq0mo  7762  addnnnq0  7763  mulnnnq0  7764  nqnq0a  7768  nqnq0m  7769  nq0a0  7771  nq02m  7779  genpdf  7822  genipv  7823  genpelxp  7825  addcomprg  7892  mulcomprg  7894  prplnqu  7934  cauappcvgprlemlim  7975  caucvgprprlemell  7999  caucvgprprlemelu  8000  caucvgprprlemcbv  8001  caucvgprprlemval  8002  caucvgprprlemnkeqj  8004  caucvgprprlemml  8008  caucvgprprlemmu  8009  caucvgprprlemopl  8011  caucvgprprlemlol  8012  caucvgprprlemopu  8013  caucvgprprlemloc  8017  caucvgprprlemclphr  8019  caucvgprprlemexbt  8020  caucvgprprlem1  8023  caucvgprprlem2  8024  addsrmo  8057  mulsrmo  8058  addsrpr  8059  mulsrpr  8060  caucvgsr  8116  addcnsr  8148  mulcnsr  8149  mulresr  8152  pitonnlem2  8161  pitonn  8162  recidpipr  8170  axaddcom  8184  ax0id  8192  axcnre  8195  nntopi  8208  axcaucvglemval  8211  frecuzrdgrrn  10769  frec2uzrdg  10770  frecuzrdgrcl  10771  frecuzrdgsuc  10775  frecuzrdgrclt  10776  frecuzrdgg  10777  frecuzrdgsuctlem  10784  seqeq1  10811  iseqvalcbv  10820  seq3val  10821  seqvalcd  10822  pfxsuff1eqwrdeq  11387  swrdpfx  11395  ccatopth  11404  swrdccatin2d  11432  eucalgval2  12746  qnumdenbi  12885  crth  12917  phimullem  12918  ennnfonelemg  13146  ennnfonelem1  13150  ressval3d  13277  imasex  13510  imasival  13511  imasaddvallemg  13520  xpsff1o  13554  txcnp  15128  upxp  15129  uptx  15131  txlm  15136  cnmpt1t  15142  cnmpt2t  15150  txhmeo  15176  pellexlem3  15839  mpodvdsmulf1o  15850