Theorem opeq12d 3830

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

Syntax hints:   → wi 4   = wceq 1373  ⟨cop 3638

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3172  df-sn 3641  df-pr 3642  df-op 3644

This theorem is referenced by:  nfopd  3839  moop2  4301  funopsn  5772  fliftfuns  5877  elxp6  6265  dfmpo  6319  tfrlemi1  6428  qliftfuns  6716  xpassen  6937  xpdom2  6938  xpf1o  6953  xpmapenlem  6958  xpmapen  6959  dfplpq2  7480  dfmpq2  7481  addpipqqs  7496  mulpipq2  7497  mulpipq  7498  mulpipqqs  7499  mulidnq  7515  addnq0mo  7573  mulnq0mo  7574  addnnnq0  7575  mulnnnq0  7576  nqnq0a  7580  nqnq0m  7581  nq0a0  7583  nq02m  7591  genpdf  7634  genipv  7635  genpelxp  7637  addcomprg  7704  mulcomprg  7706  prplnqu  7746  cauappcvgprlemlim  7787  caucvgprprlemell  7811  caucvgprprlemelu  7812  caucvgprprlemcbv  7813  caucvgprprlemval  7814  caucvgprprlemnkeqj  7816  caucvgprprlemml  7820  caucvgprprlemmu  7821  caucvgprprlemopl  7823  caucvgprprlemlol  7824  caucvgprprlemopu  7825  caucvgprprlemloc  7829  caucvgprprlemclphr  7831  caucvgprprlemexbt  7832  caucvgprprlem1  7835  caucvgprprlem2  7836  addsrmo  7869  mulsrmo  7870  addsrpr  7871  mulsrpr  7872  caucvgsr  7928  addcnsr  7960  mulcnsr  7961  mulresr  7964  pitonnlem2  7973  pitonn  7974  recidpipr  7982  axaddcom  7996  ax0id  8004  axcnre  8007  nntopi  8020  axcaucvglemval  8023  frecuzrdgrrn  10566  frec2uzrdg  10567  frecuzrdgrcl  10568  frecuzrdgsuc  10572  frecuzrdgrclt  10573  frecuzrdgg  10574  frecuzrdgsuctlem  10581  seqeq1  10608  iseqvalcbv  10617  seq3val  10618  seqvalcd  10619  pfxsuff1eqwrdeq  11164  swrdpfx  11172  eucalgval2  12425  qnumdenbi  12564  crth  12596  phimullem  12597  ennnfonelemg  12824  ennnfonelem1  12828  ressval3d  12954  imasex  13187  imasival  13188  imasaddvallemg  13197  xpsff1o  13231  txcnp  14793  upxp  14794  uptx  14796  txlm  14801  cnmpt1t  14807  cnmpt2t  14815  txhmeo  14841  mpodvdsmulf1o  15512