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

Theorem ineqan12d 4188
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 4181 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3syl2an 595 1 ((𝜑𝜓) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  cin 3932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1531  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-rab 3144  df-in 3940
This theorem is referenced by:  funprg  6401  funtpg  6402  funcnvpr  6409  funcnvqp  6411  fvun1  6747  fndmin  6807  offval  7405  ofrfval  7406  offval3  7672  fpar  7800  offsplitfpar  7804  wfrlem4  7947  fisn  8879  ixxin  12743  vdwmc  16302  fvcosymgeq  18486  cssincl  20760  inmbl  24070  iundisj2  24077  itg1addlem3  24226  fh1  29322  iundisj2f  30268  iundisj2fi  30446  satffunlem1lem1  32546  satffunlem2lem1  32548  br1cosscnvxrn  35594
  Copyright terms: Public domain W3C validator