Theorem opeq12d 3788

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

Syntax hints:   → wi 4   = wceq 1353  ⟨cop 3597

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603

This theorem is referenced by:  nfopd  3797  moop2  4253  fliftfuns  5801  elxp6  6172  dfmpo  6226  tfrlemi1  6335  qliftfuns  6621  xpassen  6832  xpdom2  6833  xpf1o  6846  xpmapenlem  6851  xpmapen  6852  dfplpq2  7355  dfmpq2  7356  addpipqqs  7371  mulpipq2  7372  mulpipq  7373  mulpipqqs  7374  mulidnq  7390  addnq0mo  7448  mulnq0mo  7449  addnnnq0  7450  mulnnnq0  7451  nqnq0a  7455  nqnq0m  7456  nq0a0  7458  nq02m  7466  genpdf  7509  genipv  7510  genpelxp  7512  addcomprg  7579  mulcomprg  7581  prplnqu  7621  cauappcvgprlemlim  7662  caucvgprprlemell  7686  caucvgprprlemelu  7687  caucvgprprlemcbv  7688  caucvgprprlemval  7689  caucvgprprlemnkeqj  7691  caucvgprprlemml  7695  caucvgprprlemmu  7696  caucvgprprlemopl  7698  caucvgprprlemlol  7699  caucvgprprlemopu  7700  caucvgprprlemloc  7704  caucvgprprlemclphr  7706  caucvgprprlemexbt  7707  caucvgprprlem1  7710  caucvgprprlem2  7711  addsrmo  7744  mulsrmo  7745  addsrpr  7746  mulsrpr  7747  caucvgsr  7803  addcnsr  7835  mulcnsr  7836  mulresr  7839  pitonnlem2  7848  pitonn  7849  recidpipr  7857  axaddcom  7871  ax0id  7879  axcnre  7882  nntopi  7895  axcaucvglemval  7898  frecuzrdgrrn  10410  frec2uzrdg  10411  frecuzrdgrcl  10412  frecuzrdgsuc  10416  frecuzrdgrclt  10417  frecuzrdgg  10418  frecuzrdgsuctlem  10425  seqeq1  10450  iseqvalcbv  10459  seq3val  10460  seqvalcd  10461  eucalgval2  12055  qnumdenbi  12194  crth  12226  phimullem  12227  ennnfonelemg  12406  ennnfonelem1  12410  ressval3d  12533  imasex  12731  imasival  12732  imasaddvallemg  12741  xpsff1o  12773  txcnp  13810  upxp  13811  uptx  13813  txlm  13818  cnmpt1t  13824  cnmpt2t  13832  txhmeo  13858