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

Theorem ineqan12d 4214
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 4207 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3syl2an 595 1 ((𝜑𝜓) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  cin 3947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-in 3955
This theorem is referenced by:  funprg  6602  funtpg  6603  funcnvpr  6610  funcnvqp  6612  fvun1  6982  fndmin  7046  ofrfvalg  7682  offval  7683  offval3  7973  fpar  8106  offsplitfpar  8109  wfrlem4OLD  8316  fisn  9426  ixxin  13346  vdwmc  16916  fvcosymgeq  19339  cssincl  21461  inmbl  25292  iundisj2  25299  itg1addlem3  25448  fh1  31139  iundisj2f  32089  iundisj2fi  32276  satffunlem1lem1  34692  satffunlem2lem1  34694  disjeccnvep  37456  disjecxrn  37563  br1cosscnvxrn  37648
  Copyright terms: Public domain W3C validator