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

Theorem ineqan12d 4189
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 4182 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3syl2an 597 1 ((𝜑𝜓) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398   = wceq 1530  cin 3933
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1533  df-ex 1774  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-rab 3145  df-in 3941
This theorem is referenced by:  funprg  6401  funtpg  6402  funcnvpr  6409  funcnvqp  6411  fvun1  6747  fndmin  6808  offval  7408  ofrfval  7409  offval3  7675  fpar  7803  offsplitfpar  7807  wfrlem4  7950  fisn  8883  ixxin  12747  vdwmc  16306  fvcosymgeq  18549  cssincl  20824  inmbl  24135  iundisj2  24142  itg1addlem3  24291  fh1  29387  iundisj2f  30332  iundisj2fi  30512  satffunlem1lem1  32637  satffunlem2lem1  32639  br1cosscnvxrn  35701
  Copyright terms: Public domain W3C validator