Theorem opeq12d 3910

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

Syntax hints:   → wi 4   = wceq 1402  ⟨cop 3711

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3714  df-pr 3715  df-op 3717

This theorem is referenced by:  nfopd  3919  moop2  4390  fsn2g  5877  funopsn  5885  fliftfuns  5998  elxp6  6397  dfmpo  6453  tfrlemi1  6597  qliftfuns  6887  xpassen  7122  xpdom2  7123  xpf1o  7138  xpmapenlem  7143  xpmapen  7144  mapunen  7145  dfplpq2  7715  dfmpq2  7716  addpipqqs  7731  mulpipq2  7732  mulpipq  7733  mulpipqqs  7734  mulidnq  7750  addnq0mo  7808  mulnq0mo  7809  addnnnq0  7810  mulnnnq0  7811  nqnq0a  7815  nqnq0m  7816  nq0a0  7818  nq02m  7826  genpdf  7869  genipv  7870  genpelxp  7872  addcomprg  7939  mulcomprg  7941  prplnqu  7981  cauappcvgprlemlim  8022  caucvgprprlemell  8046  caucvgprprlemelu  8047  caucvgprprlemcbv  8048  caucvgprprlemval  8049  caucvgprprlemnkeqj  8051  caucvgprprlemml  8055  caucvgprprlemmu  8056  caucvgprprlemopl  8058  caucvgprprlemlol  8059  caucvgprprlemopu  8060  caucvgprprlemloc  8064  caucvgprprlemclphr  8066  caucvgprprlemexbt  8067  caucvgprprlem1  8070  caucvgprprlem2  8071  addsrmo  8104  mulsrmo  8105  addsrpr  8106  mulsrpr  8107  caucvgsr  8163  addcnsr  8195  mulcnsr  8196  mulresr  8199  pitonnlem2  8208  pitonn  8209  recidpipr  8217  axaddcom  8231  ax0id  8239  axcnre  8242  nntopi  8255  axcaucvglemval  8258  frecuzrdgrrn  10828  frec2uzrdg  10829  frecuzrdgrcl  10830  frecuzrdgsuc  10834  frecuzrdgrclt  10835  frecuzrdgg  10836  frecuzrdgsuctlem  10843  seqeq1  10870  iseqvalcbv  10879  seq3val  10880  seqvalcd  10881  pfxsuff1eqwrdeq  11454  swrdpfx  11462  ccatopth  11471  swrdccatin2d  11499  eucalgval2  12814  qnumdenbi  12953  crth  12985  phimullem  12986  ennnfonelemg  13277  ennnfonelem1  13281  ressval3d  13409  imasex  13609  imasival  13610  imasaddvallemg  13619  xpsff1o  13653  txcnp  15355  upxp  15356  uptx  15358  txlm  15363  cnmpt1t  15369  cnmpt2t  15377  txhmeo  15403  pellexlem3  16076  mpodvdsmulf1o  16087