Theorem opeq12d 3865

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

Syntax hints:   → wi 4   = wceq 1395  ⟨cop 3669

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675

This theorem is referenced by:  nfopd  3874  moop2  4338  funopsn  5819  fliftfuns  5928  elxp6  6321  dfmpo  6375  tfrlemi1  6484  qliftfuns  6774  xpassen  6997  xpdom2  6998  xpf1o  7013  xpmapenlem  7018  xpmapen  7019  dfplpq2  7549  dfmpq2  7550  addpipqqs  7565  mulpipq2  7566  mulpipq  7567  mulpipqqs  7568  mulidnq  7584  addnq0mo  7642  mulnq0mo  7643  addnnnq0  7644  mulnnnq0  7645  nqnq0a  7649  nqnq0m  7650  nq0a0  7652  nq02m  7660  genpdf  7703  genipv  7704  genpelxp  7706  addcomprg  7773  mulcomprg  7775  prplnqu  7815  cauappcvgprlemlim  7856  caucvgprprlemell  7880  caucvgprprlemelu  7881  caucvgprprlemcbv  7882  caucvgprprlemval  7883  caucvgprprlemnkeqj  7885  caucvgprprlemml  7889  caucvgprprlemmu  7890  caucvgprprlemopl  7892  caucvgprprlemlol  7893  caucvgprprlemopu  7894  caucvgprprlemloc  7898  caucvgprprlemclphr  7900  caucvgprprlemexbt  7901  caucvgprprlem1  7904  caucvgprprlem2  7905  addsrmo  7938  mulsrmo  7939  addsrpr  7940  mulsrpr  7941  caucvgsr  7997  addcnsr  8029  mulcnsr  8030  mulresr  8033  pitonnlem2  8042  pitonn  8043  recidpipr  8051  axaddcom  8065  ax0id  8073  axcnre  8076  nntopi  8089  axcaucvglemval  8092  frecuzrdgrrn  10638  frec2uzrdg  10639  frecuzrdgrcl  10640  frecuzrdgsuc  10644  frecuzrdgrclt  10645  frecuzrdgg  10646  frecuzrdgsuctlem  10653  seqeq1  10680  iseqvalcbv  10689  seq3val  10690  seqvalcd  10691  pfxsuff1eqwrdeq  11239  swrdpfx  11247  ccatopth  11256  swrdccatin2d  11284  eucalgval2  12583  qnumdenbi  12722  crth  12754  phimullem  12755  ennnfonelemg  12982  ennnfonelem1  12986  ressval3d  13113  imasex  13346  imasival  13347  imasaddvallemg  13356  xpsff1o  13390  txcnp  14953  upxp  14954  uptx  14956  txlm  14961  cnmpt1t  14967  cnmpt2t  14975  txhmeo  15001  mpodvdsmulf1o  15672