Theorem ineq12i 3812

Description: Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)

Hypotheses

Ref	Expression
ineq1i.1	|- A = B
ineq12i.2	|- C = D

Assertion

Ref	Expression
ineq12i	|- ( A i^i C ) = ( B i^i D )

Proof of Theorem ineq12i

Step	Hyp	Ref	Expression
1		ineq1i.1	. 2 |- A = B
2		ineq12i.2	. 2 |- C = D
3		ineq12 3809	. 2 |- ( ( A = B /\ C = D ) -> ( A i^i C ) = ( B i^i D ) )
4	1, 2, 3	mp2an 708	1 |- ( A i^i C ) = ( B i^i D )

Syntax hints:   = wceq 1483   i^i cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581

This theorem is referenced by:  undir  3876  difundi  3879  difindir  3882  inrab  3899  inrab2  3900  elneldisj  3963  elneldisjOLD  3965  dfif4  4101  dfif5  4102  inxp  5254  resindi  5412  resindir  5413  rnin  5542  inimass  5549  predin  5703  funtp  5945  orduniss2  7033  offres  7163  fodomr  8111  wemapwe  8594  cotr3  13717  explecnv  14597  psssdm2  17215  ablfacrp  18465  cnfldfun  19758  pjfval2  20053  ofco2  20257  iundisj2  23317  lejdiri  28398  cmbr3i  28459  nonbooli  28510  5oai  28520  3oalem5  28525  mayetes3i  28588  mdexchi  29194  disjpreima  29397  disjxpin  29401  iundisj2f  29403  xppreima  29449  iundisj2fi  29556  xpinpreima  29952  xpinpreima2  29953  ordtcnvNEW  29966  pprodcnveq  31990  dfiota3  32030  bj-inrab  32923  ptrest  33408  ftc1anclem6  33490  dnwech  37618  fgraphopab  37788  onfrALTlem5  38757  onfrALTlem4  38758  onfrALTlem5VD  39121  onfrALTlem4VD  39122  disjxp1  39238  disjinfi  39380