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  4339  funopsn  5822  fliftfuns  5931  elxp6  6324  dfmpo  6380  tfrlemi1  6489  qliftfuns  6779  xpassen  7002  xpdom2  7003  xpf1o  7018  xpmapenlem  7023  xpmapen  7024  dfplpq2  7557  dfmpq2  7558  addpipqqs  7573  mulpipq2  7574  mulpipq  7575  mulpipqqs  7576  mulidnq  7592  addnq0mo  7650  mulnq0mo  7651  addnnnq0  7652  mulnnnq0  7653  nqnq0a  7657  nqnq0m  7658  nq0a0  7660  nq02m  7668  genpdf  7711  genipv  7712  genpelxp  7714  addcomprg  7781  mulcomprg  7783  prplnqu  7823  cauappcvgprlemlim  7864  caucvgprprlemell  7888  caucvgprprlemelu  7889  caucvgprprlemcbv  7890  caucvgprprlemval  7891  caucvgprprlemnkeqj  7893  caucvgprprlemml  7897  caucvgprprlemmu  7898  caucvgprprlemopl  7900  caucvgprprlemlol  7901  caucvgprprlemopu  7902  caucvgprprlemloc  7906  caucvgprprlemclphr  7908  caucvgprprlemexbt  7909  caucvgprprlem1  7912  caucvgprprlem2  7913  addsrmo  7946  mulsrmo  7947  addsrpr  7948  mulsrpr  7949  caucvgsr  8005  addcnsr  8037  mulcnsr  8038  mulresr  8041  pitonnlem2  8050  pitonn  8051  recidpipr  8059  axaddcom  8073  ax0id  8081  axcnre  8084  nntopi  8097  axcaucvglemval  8100  frecuzrdgrrn  10647  frec2uzrdg  10648  frecuzrdgrcl  10649  frecuzrdgsuc  10653  frecuzrdgrclt  10654  frecuzrdgg  10655  frecuzrdgsuctlem  10662  seqeq1  10689  iseqvalcbv  10698  seq3val  10699  seqvalcd  10700  pfxsuff1eqwrdeq  11252  swrdpfx  11260  ccatopth  11269  swrdccatin2d  11297  eucalgval2  12596  qnumdenbi  12735  crth  12767  phimullem  12768  ennnfonelemg  12995  ennnfonelem1  12999  ressval3d  13126  imasex  13359  imasival  13360  imasaddvallemg  13369  xpsff1o  13403  txcnp  14966  upxp  14967  uptx  14969  txlm  14974  cnmpt1t  14980  cnmpt2t  14988  txhmeo  15014  mpodvdsmulf1o  15685