Theorem opeq12d 3813

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

Syntax hints:   → wi 4   = wceq 1364  ⟨cop 3622

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628

This theorem is referenced by:  nfopd  3822  moop2  4281  fliftfuns  5842  elxp6  6224  dfmpo  6278  tfrlemi1  6387  qliftfuns  6675  xpassen  6886  xpdom2  6887  xpf1o  6902  xpmapenlem  6907  xpmapen  6908  dfplpq2  7416  dfmpq2  7417  addpipqqs  7432  mulpipq2  7433  mulpipq  7434  mulpipqqs  7435  mulidnq  7451  addnq0mo  7509  mulnq0mo  7510  addnnnq0  7511  mulnnnq0  7512  nqnq0a  7516  nqnq0m  7517  nq0a0  7519  nq02m  7527  genpdf  7570  genipv  7571  genpelxp  7573  addcomprg  7640  mulcomprg  7642  prplnqu  7682  cauappcvgprlemlim  7723  caucvgprprlemell  7747  caucvgprprlemelu  7748  caucvgprprlemcbv  7749  caucvgprprlemval  7750  caucvgprprlemnkeqj  7752  caucvgprprlemml  7756  caucvgprprlemmu  7757  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemopu  7761  caucvgprprlemloc  7765  caucvgprprlemclphr  7767  caucvgprprlemexbt  7768  caucvgprprlem1  7771  caucvgprprlem2  7772  addsrmo  7805  mulsrmo  7806  addsrpr  7807  mulsrpr  7808  caucvgsr  7864  addcnsr  7896  mulcnsr  7897  mulresr  7900  pitonnlem2  7909  pitonn  7910  recidpipr  7918  axaddcom  7932  ax0id  7940  axcnre  7943  nntopi  7956  axcaucvglemval  7959  frecuzrdgrrn  10482  frec2uzrdg  10483  frecuzrdgrcl  10484  frecuzrdgsuc  10488  frecuzrdgrclt  10489  frecuzrdgg  10490  frecuzrdgsuctlem  10497  seqeq1  10524  iseqvalcbv  10533  seq3val  10534  seqvalcd  10535  eucalgval2  12194  qnumdenbi  12333  crth  12365  phimullem  12366  ennnfonelemg  12563  ennnfonelem1  12567  ressval3d  12693  imasex  12891  imasival  12892  imasaddvallemg  12901  xpsff1o  12935  txcnp  14450  upxp  14451  uptx  14453  txlm  14458  cnmpt1t  14464  cnmpt2t  14472  txhmeo  14498