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

Theorem ineqan12d 3967
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 3960 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3syl2an 583 1 ((𝜑𝜓) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1631  cin 3722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730
This theorem is referenced by:  funprg  6083  funtpg  6084  funcnvpr  6091  funcnvqp  6093  fvun1  6411  fndmin  6467  offval  7051  ofrfval  7052  offval3  7309  fpar  7432  wfrlem4  7570  wfrlem4OLD  7571  fisn  8489  ixxin  12397  vdwmc  15889  fvcosymgeq  18056  cssincl  20249  inmbl  23530  iundisj2  23537  itg1addlem3  23685  fh1  28817  iundisj2f  29741  iundisj2fi  29896  br1cosscnvxrn  34566  offval0  42827
  Copyright terms: Public domain W3C validator