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

Theorem ineqan12d 4206
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 4199 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3syl2an 595 1 ((𝜑𝜓) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1533  cin 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-in 3947
This theorem is referenced by:  funprg  6592  funtpg  6593  funcnvpr  6600  funcnvqp  6602  fvun1  6972  fndmin  7036  ofrfvalg  7671  offval  7672  offval3  7962  fpar  8096  offsplitfpar  8099  wfrlem4OLD  8307  fisn  9417  ixxin  13337  vdwmc  16909  fvcosymgeq  19338  cssincl  21548  inmbl  25392  iundisj2  25399  itg1addlem3  25548  fh1  31306  iundisj2f  32256  iundisj2fi  32443  satffunlem1lem1  34848  satffunlem2lem1  34850  disjeccnvep  37608  disjecxrn  37715  br1cosscnvxrn  37800
  Copyright terms: Public domain W3C validator