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

Theorem ineqan12d 4215
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 4208 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3syl2an 594 1 ((𝜑𝜓) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1534  cin 3946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-in 3954
This theorem is referenced by:  funprg  6613  funtpg  6614  funcnvpr  6621  funcnvqp  6623  fvun1  6993  fndmin  7058  ofrfvalg  7698  offval  7699  offval3  7996  fpar  8130  offsplitfpar  8133  wfrlem4OLD  8342  fisn  9470  ixxin  13395  vdwmc  16980  fvcosymgeq  19427  cssincl  21684  inmbl  25562  iundisj2  25569  itg1addlem3  25718  fh1  31551  iundisj2f  32510  of0r  32596  iundisj2fi  32699  satffunlem1lem1  35230  satffunlem2lem1  35232  disjeccnvep  37982  disjecxrn  38087  br1cosscnvxrn  38172
  Copyright terms: Public domain W3C validator