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

Theorem ifbieq12d 3811
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 3806 . 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 3804 . 2  |-  ( ph  ->  if ( ch ,  A ,  B )  =  if ( ch ,  C ,  D )
)
62, 5eqtrd 2470 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  C ,  D )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369   ifcif 3786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-un 3328  df-if 3787
This theorem is referenced by:  csbif  3834  csbifgOLD  3835  tz7.44-2  6855  tz7.44-3  6856  boxcutc  7298  unxpdomlem1  7509  dfac12lem1  8304  dfac12r  8307  fin23lem12  8492  fin23lem33  8506  ttukeylem3  8672  ttukey2g  8677  xaddval  11185  seqf1olem2  11838  expval  11859  ccatfval  12265  ccatval1  12268  ccatval2  12269  ruclem1  13505  eucalgval2  13748  ressval  14217  gsumvalx  15493  gsumpropd  15495  gsumpropd2lem  15496  gsumress  15498  mulgval  15620  pmtrval  15948  pmtrfv  15949  mvrfval  17470  xrsdsval  17832  marrepeval  18349  marepveval  18354  mdetunilem9  18401  maducoeval  18420  maducoeval2  18421  madutpos  18423  madugsum  18424  minmar1eval  18430  symgmatr01lem  18434  symgmatr01  18435  gsummatr01lem3  18438  gsummatr01lem4  18439  gsummatr01  18440  ptcmplem3  19601  xrhmeo  20493  phtpycc  20538  pcovalg  20559  pcocn  20564  pcohtpylem  20566  pcoass  20571  pcorevlem  20573  ovolunlem1a  20954  ovolunlem1  20955  ioombl1  21018  mbfmax  21102  mbfpos  21104  mbfi1fseqlem2  21169  mbfi1fseq  21174  ditgeq1  21298  ditgeq2  21299  ig1pval  21619  cxpval  22084  musumsum  22507  muinv  22508  lgsval  22614  gxval  23696  resvval  26247  ballotlemsval  26843  ballotlemsv  26844  ballotlemsf1o  26848  ballotlemieq  26851  plymulx0  26900  lgamgulmlem4  26970  lgamgulmlem5  26971  cbvprod  27379  prodmolem2a  27398  zprod  27401  fprod  27405  fprodntriv  27406  prodss  27411  rdgprc0  27558  dfrdg2  27560  mblfinlem2  28382  itg2addnclem3  28398  itgaddnclem2  28404  ftc1anclem5  28424  ftc1anclem6  28425  aomclem8  29367  afveq12d  29992  clwlkisclwwlklem2fv1  30397  cdleme27b  33852  cdleme29b  33859  cdleme31sn  33864  cdleme31fv  33874  cdleme40v  33953  cdlemk40  34401  dihffval  34715  dihfval  34716  dihval  34717
  Copyright terms: Public domain W3C validator