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

Theorem ineqan12d 4222
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 4215 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3syl2an 596 1 ((𝜑𝜓) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  cin 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958
This theorem is referenced by:  funprg  6620  funtpg  6621  funcnvpr  6628  funcnvqp  6630  fvun1  7000  fndmin  7065  ofrfvalg  7705  offval  7706  offval3  8007  fpar  8141  offsplitfpar  8144  wfrlem4OLD  8352  fisn  9467  ixxin  13404  vdwmc  17016  fvcosymgeq  19447  cssincl  21706  inmbl  25577  iundisj2  25584  itg1addlem3  25733  fh1  31637  iundisj2f  32603  of0r  32688  iundisj2fi  32799  satffunlem1lem1  35407  satffunlem2lem1  35409  disjeccnvep  38285  disjecxrn  38390  br1cosscnvxrn  38475
  Copyright terms: Public domain W3C validator