MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ineqan12d Structured version   Visualization version   GIF version

Theorem ineqan12d 4229
Description: Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007.)
Hypotheses
Ref Expression
ineq1d.1 (𝜑𝐴 = 𝐵)
ineqan12d.2 (𝜓𝐶 = 𝐷)
Assertion
Ref Expression
ineqan12d ((𝜑𝜓) → (𝐴𝐶) = (𝐵𝐷))

Proof of Theorem ineqan12d
StepHypRef Expression
1 ineq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 ineqan12d.2 . 2 (𝜓𝐶 = 𝐷)
3 ineq12 4222 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3syl2an 596 1 ((𝜑𝜓) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1536  cin 3961
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-in 3969
This theorem is referenced by:  funprg  6621  funtpg  6622  funcnvpr  6629  funcnvqp  6631  fvun1  6999  fndmin  7064  ofrfvalg  7704  offval  7705  offval3  8005  fpar  8139  offsplitfpar  8142  wfrlem4OLD  8350  fisn  9464  ixxin  13400  vdwmc  17011  fvcosymgeq  19461  cssincl  21723  inmbl  25590  iundisj2  25597  itg1addlem3  25746  fh1  31646  iundisj2f  32609  of0r  32694  iundisj2fi  32804  satffunlem1lem1  35386  satffunlem2lem1  35388  disjeccnvep  38265  disjecxrn  38370  br1cosscnvxrn  38455
  Copyright terms: Public domain W3C validator