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

Theorem ifbieq12d 3966
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 3961 . 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 3959 . 2  |-  ( ph  ->  if ( ch ,  A ,  B )  =  if ( ch ,  C ,  D )
)
62, 5eqtrd 2508 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  C ,  D )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379   ifcif 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-un 3481  df-if 3940
This theorem is referenced by:  csbif  3989  csbifgOLD  3990  tz7.44-2  7070  tz7.44-3  7071  boxcutc  7509  unxpdomlem1  7721  dfac12lem1  8519  dfac12r  8522  fin23lem12  8707  fin23lem33  8721  ttukeylem3  8887  ttukey2g  8892  xaddval  11418  seqf1olem2  12110  expval  12131  ccatfval  12551  ccatval1  12554  ccatval2  12555  ruclem1  13818  eucalgval2  14062  ressval  14535  gsumvalx  15812  gsumpropd  15814  gsumpropd2lem  15815  gsumress  15817  mulgval  15941  pmtrval  16269  pmtrfv  16270  mvrfval  17844  xrsdsval  18227  marrepeval  18829  marepveval  18834  mdetunilem9  18886  maducoeval  18905  maducoeval2  18906  madutpos  18908  madugsum  18909  minmar1eval  18915  symgmatr01lem  18919  symgmatr01  18920  gsummatr01lem3  18923  gsummatr01lem4  18924  gsummatr01  18925  fvmptnn04if  19114  ptcmplem3  20286  xrhmeo  21178  phtpycc  21223  pcovalg  21244  pcocn  21249  pcohtpylem  21251  pcoass  21256  pcorevlem  21258  ovolunlem1a  21639  ovolunlem1  21640  ioombl1  21704  mbfmax  21788  mbfpos  21790  mbfi1fseqlem2  21855  mbfi1fseq  21860  ditgeq1  21984  ditgeq2  21985  ig1pval  22305  cxpval  22770  musumsum  23193  muinv  23194  lgsval  23300  clwlkisclwwlklem2fv1  24455  gxval  24933  resvval  27477  ballotlemsval  28084  ballotlemsv  28085  ballotlemsf1o  28089  ballotlemieq  28092  plymulx0  28141  lgamgulmlem4  28211  lgamgulmlem5  28212  cbvprod  28621  prodmolem2a  28640  zprod  28643  fprod  28647  fprodntriv  28648  prodss  28653  rdgprc0  28800  dfrdg2  28802  mblfinlem2  29627  itg2addnclem3  29643  itgaddnclem2  29649  ftc1anclem5  29669  ftc1anclem6  29670  aomclem8  30611  icccncfext  31226  afveq12d  31685  cdleme27b  35164  cdleme29b  35171  cdleme31sn  35176  cdleme31fv  35186  cdleme40v  35265  cdlemk40  35713  dihffval  36027  dihfval  36028  dihval  36029
  Copyright terms: Public domain W3C validator