MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifbieq12d Structured version   Unicode version

Theorem ifbieq12d 3804
Description: Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypotheses
Ref Expression
ifbieq12d.1  |-  ( ph  ->  ( ps  <->  ch )
)
ifbieq12d.2  |-  ( ph  ->  A  =  C )
ifbieq12d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
ifbieq12d  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  C ,  D )
)

Proof of Theorem ifbieq12d
StepHypRef Expression
1 ifbieq12d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21ifbid 3799 . 2  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  A ,  B )
)
3 ifbieq12d.2 . . 3  |-  ( ph  ->  A  =  C )
4 ifbieq12d.3 . . 3  |-  ( ph  ->  B  =  D )
53, 4ifeq12d 3797 . 2  |-  ( ph  ->  if ( ch ,  A ,  B )  =  if ( ch ,  C ,  D )
)
62, 5eqtrd 2465 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  C ,  D )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1362   ifcif 3779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-un 3321  df-if 3780
This theorem is referenced by:  csbif  3827  csbifgOLD  3828  tz7.44-2  6849  tz7.44-3  6850  boxcutc  7294  unxpdomlem1  7505  dfac12lem1  8300  dfac12r  8303  fin23lem12  8488  fin23lem33  8502  ttukeylem3  8668  ttukey2g  8673  xaddval  11181  seqf1olem2  11830  expval  11851  ccatfval  12257  ccatval1  12260  ccatval2  12261  ruclem1  13496  eucalgval2  13739  ressval  14208  gsumvalx  15484  gsumpropd  15486  gsumress  15487  mulgval  15609  pmtrval  15937  pmtrfv  15938  mvrfval  17427  xrsdsval  17701  marrepeval  18216  marepveval  18221  mdetunilem9  18268  maducoeval  18287  maducoeval2  18288  madutpos  18290  madugsum  18291  minmar1eval  18297  symgmatr01lem  18301  symgmatr01  18302  gsummatr01lem3  18305  gsummatr01lem4  18306  gsummatr01  18307  ptcmplem3  19468  xrhmeo  20360  phtpycc  20405  pcovalg  20426  pcocn  20431  pcohtpylem  20433  pcoass  20438  pcorevlem  20440  ovolunlem1a  20821  ovolunlem1  20822  ioombl1  20885  mbfmax  20969  mbfpos  20971  mbfi1fseqlem2  21036  mbfi1fseq  21041  ditgeq1  21165  ditgeq2  21166  ig1pval  21529  cxpval  21994  musumsum  22417  muinv  22418  lgsval  22524  gxval  23568  gsumpropd2lem  26093  resvval  26149  ballotlemsval  26739  ballotlemsv  26740  ballotlemsf1o  26744  ballotlemieq  26747  plymulx0  26796  lgamgulmlem4  26866  lgamgulmlem5  26867  cbvprod  27275  prodmolem2a  27294  zprod  27297  fprod  27301  fprodntriv  27302  prodss  27307  rdgprc0  27454  dfrdg2  27456  mblfinlem2  28273  itg2addnclem  28287  itg2addnclem3  28289  itgaddnclem2  28295  ftc1anclem5  28315  ftc1anclem6  28316  aomclem8  29259  afveq12d  29885  clwlkisclwwlklem2fv1  30290  cdleme27b  33585  cdleme29b  33592  cdleme31sn  33597  cdleme31fv  33607  cdleme40v  33686  cdlemk40  34134  dihffval  34448  dihfval  34449  dihval  34450
  Copyright terms: Public domain W3C validator