Theorem opeq12d 3773

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

Syntax hints:   → wi 4   = wceq 1348  ⟨cop 3586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592

This theorem is referenced by:  nfopd  3782  moop2  4236  fliftfuns  5777  elxp6  6148  dfmpo  6202  tfrlemi1  6311  qliftfuns  6597  xpassen  6808  xpdom2  6809  xpf1o  6822  xpmapenlem  6827  xpmapen  6828  dfplpq2  7316  dfmpq2  7317  addpipqqs  7332  mulpipq2  7333  mulpipq  7334  mulpipqqs  7335  mulidnq  7351  addnq0mo  7409  mulnq0mo  7410  addnnnq0  7411  mulnnnq0  7412  nqnq0a  7416  nqnq0m  7417  nq0a0  7419  nq02m  7427  genpdf  7470  genipv  7471  genpelxp  7473  addcomprg  7540  mulcomprg  7542  prplnqu  7582  cauappcvgprlemlim  7623  caucvgprprlemell  7647  caucvgprprlemelu  7648  caucvgprprlemcbv  7649  caucvgprprlemval  7650  caucvgprprlemnkeqj  7652  caucvgprprlemml  7656  caucvgprprlemmu  7657  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemopu  7661  caucvgprprlemloc  7665  caucvgprprlemclphr  7667  caucvgprprlemexbt  7668  caucvgprprlem1  7671  caucvgprprlem2  7672  addsrmo  7705  mulsrmo  7706  addsrpr  7707  mulsrpr  7708  caucvgsr  7764  addcnsr  7796  mulcnsr  7797  mulresr  7800  pitonnlem2  7809  pitonn  7810  recidpipr  7818  axaddcom  7832  ax0id  7840  axcnre  7843  nntopi  7856  axcaucvglemval  7859  frecuzrdgrrn  10364  frec2uzrdg  10365  frecuzrdgrcl  10366  frecuzrdgsuc  10370  frecuzrdgrclt  10371  frecuzrdgg  10372  frecuzrdgsuctlem  10379  seqeq1  10404  iseqvalcbv  10413  seq3val  10414  seqvalcd  10415  eucalgval2  12007  qnumdenbi  12146  crth  12178  phimullem  12179  ennnfonelemg  12358  ennnfonelem1  12362  txcnp  13065  upxp  13066  uptx  13068  txlm  13073  cnmpt1t  13079  cnmpt2t  13087  txhmeo  13113