Theorem opeq12d 3893

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

Syntax hints:   → wi 4   = wceq 1398  ⟨cop 3694

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700

This theorem is referenced by:  nfopd  3902  moop2  4370  fsn2g  5854  funopsn  5862  fliftfuns  5973  elxp6  6365  dfmpo  6421  tfrlemi1  6565  qliftfuns  6855  xpassen  7083  xpdom2  7084  xpf1o  7099  xpmapenlem  7104  xpmapen  7105  mapunen  7106  dfplpq2  7671  dfmpq2  7672  addpipqqs  7687  mulpipq2  7688  mulpipq  7689  mulpipqqs  7690  mulidnq  7706  addnq0mo  7764  mulnq0mo  7765  addnnnq0  7766  mulnnnq0  7767  nqnq0a  7771  nqnq0m  7772  nq0a0  7774  nq02m  7782  genpdf  7825  genipv  7826  genpelxp  7828  addcomprg  7895  mulcomprg  7897  prplnqu  7937  cauappcvgprlemlim  7978  caucvgprprlemell  8002  caucvgprprlemelu  8003  caucvgprprlemcbv  8004  caucvgprprlemval  8005  caucvgprprlemnkeqj  8007  caucvgprprlemml  8011  caucvgprprlemmu  8012  caucvgprprlemopl  8014  caucvgprprlemlol  8015  caucvgprprlemopu  8016  caucvgprprlemloc  8020  caucvgprprlemclphr  8022  caucvgprprlemexbt  8023  caucvgprprlem1  8026  caucvgprprlem2  8027  addsrmo  8060  mulsrmo  8061  addsrpr  8062  mulsrpr  8063  caucvgsr  8119  addcnsr  8151  mulcnsr  8152  mulresr  8155  pitonnlem2  8164  pitonn  8165  recidpipr  8173  axaddcom  8187  ax0id  8195  axcnre  8198  nntopi  8211  axcaucvglemval  8214  frecuzrdgrrn  10774  frec2uzrdg  10775  frecuzrdgrcl  10776  frecuzrdgsuc  10780  frecuzrdgrclt  10781  frecuzrdgg  10782  frecuzrdgsuctlem  10789  seqeq1  10816  iseqvalcbv  10825  seq3val  10826  seqvalcd  10827  pfxsuff1eqwrdeq  11395  swrdpfx  11403  ccatopth  11412  swrdccatin2d  11440  eucalgval2  12754  qnumdenbi  12893  crth  12925  phimullem  12926  ennnfonelemg  13171  ennnfonelem1  13175  ressval3d  13302  imasex  13535  imasival  13536  imasaddvallemg  13545  xpsff1o  13579  txcnp  15153  upxp  15154  uptx  15156  txlm  15161  cnmpt1t  15167  cnmpt2t  15175  txhmeo  15201  pellexlem3  15864  mpodvdsmulf1o  15875