ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  opeq12d GIF version

Theorem opeq12d 3586
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
StepHypRef Expression
1 opeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 opeq12d.2 . 2 (𝜑𝐶 = 𝐷)
3 opeq12 3580 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
41, 2, 3syl2anc 403 1 (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285  cop 3409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604  df-un 2978  df-sn 3412  df-pr 3413  df-op 3415
This theorem is referenced by:  nfopd  3595  moop2  4014  fliftfuns  5469  elxp6  5827  dfmpt2  5875  tfrlemi1  5981  qliftfuns  6256  xpassen  6374  xpdom2  6375  xpf1o  6385  dfplpq2  6606  dfmpq2  6607  addpipqqs  6622  mulpipq2  6623  mulpipq  6624  mulpipqqs  6625  mulidnq  6641  addnq0mo  6699  mulnq0mo  6700  addnnnq0  6701  mulnnnq0  6702  nqnq0a  6706  nqnq0m  6707  nq0a0  6709  nq02m  6717  genpdf  6760  genipv  6761  genpelxp  6763  addcomprg  6830  mulcomprg  6832  prplnqu  6872  cauappcvgprlemlim  6913  caucvgprprlemell  6937  caucvgprprlemelu  6938  caucvgprprlemcbv  6939  caucvgprprlemval  6940  caucvgprprlemnkeqj  6942  caucvgprprlemml  6946  caucvgprprlemmu  6947  caucvgprprlemopl  6949  caucvgprprlemlol  6950  caucvgprprlemopu  6951  caucvgprprlemloc  6955  caucvgprprlemclphr  6957  caucvgprprlemexbt  6958  caucvgprprlem1  6961  caucvgprprlem2  6962  addsrmo  6982  mulsrmo  6983  addsrpr  6984  mulsrpr  6985  caucvgsr  7040  addcnsr  7064  mulcnsr  7065  mulresr  7068  pitonnlem2  7077  pitonn  7078  recidpipr  7086  axaddcom  7098  ax0id  7106  axcnre  7109  nntopi  7122  axcaucvglemval  7125  frecuzrdgrrn  9490  frec2uzrdg  9491  frecuzrdgrcl  9492  frecuzrdgsuc  9496  frecuzrdgrclt  9497  frecuzrdgg  9498  frecuzrdgsuctlem  9505  iseqeq1  9524  iseqvalcbv  9531  iseqvalt  9532  eucalgval2  10579
  Copyright terms: Public domain W3C validator