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

Theorem ifbieq12d 3528
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 3524 . 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 3522 . 2  |-  ( ph  ->  if ( ch ,  A ,  B )  =  if ( ch ,  C ,  D )
)
62, 5eqtrd 2288 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  C ,  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    = wceq 1619   ifcif 3506
This theorem is referenced by:  csbifg  3534  opeq1  3737  opeq2  3738  riotaeqdv  6238  riotabidv  6239  tz7.44-2  6353  tz7.44-3  6354  boxcutc  6792  unxpdomlem1  7000  oieq1  7160  oieq2  7161  cantnflem1d  7323  cantnflem1  7324  iunfictbso  7674  dfac12lem1  7702  dfac12r  7705  fin23lem12  7890  fin23lem33  7904  ttukeylem3  8071  ttukey2g  8076  xaddval  10481  seqf1olem2  11017  expval  11037  bcval  11248  ccatfval  11358  ccatval1  11361  ccatval2  11362  swrdval  11380  cbvsum  12098  summolem2a  12118  zsum  12121  fsum  12123  sumss  12127  sumss2  12129  fsumcvg2  12130  fsumser  12133  isumless  12231  rpnnen2lem1  12420  rpnnen  12432  ruclem1  12436  sadadd2lem  12577  sadadd2  12578  eucalgval2  12678  pcmpt  12867  pcmptdvds  12869  prmreclem2  12891  prmreclem4  12893  prmreclem5  12894  prmreclem6  12895  prmrec  12896  ramub1lem2  13001  ramcl  13003  ressval  13122  gsumvalx  14378  gsumpropd  14380  gsumress  14381  mulgval  14496  cyggenod2  15099  dmdprdsplitlem  15199  mvrfval  16092  evlslem2  16176  coe1tmmul2fv  16281  coe1pwmulfv  16283  xrsdsval  16342  cyggic  16453  fclsval  17630  ptcmplem3  17675  stdbdmetval  17987  stdbdxmet  17988  xrhmeo  18371  phtpycc  18416  pcovalg  18437  pcocn  18442  pcohtpylem  18444  pcopt2  18448  pcoass  18449  pcorevlem  18451  cmetcaulem  18641  ovolunlem1a  18782  ovolunlem1  18783  ovolicc2lem3  18805  ovolicc2lem4  18806  ovolicc2lem5  18807  ioombl1  18846  mbfmax  18931  mbfpos  18933  mbfposb  18935  i1fres  18987  i1fposd  18989  mbfi1fseqlem2  18998  mbfi1fseq  19003  mbfi1flimlem  19004  mbfi1flim  19005  itg2splitlem  19030  itg2cnlem1  19043  itg2cn  19045  isibl  19047  isibl2  19048  iblitg  19050  dfitg  19051  cbvitg  19057  itgeq2  19059  itgvallem  19066  iblneg  19084  itgneg  19085  itgss3  19096  itgcn  19124  ditgeq1  19125  ditgeq2  19126  deg1suble  19420  ig1pval  19485  elply2  19505  dgrsub  19580  aareccl  19633  cxpval  19938  vmaval  20278  prmorcht  20343  musumsum  20359  muinv  20360  pclogsum  20381  dchrelbasd  20405  dchrptlem2  20431  bposlem5  20454  lgsval  20466  lgsfval  20467  lgsdir  20496  lgsdilem2  20497  lgsdi  20498  lgsne0  20499  rplogsumlem2  20561  pntrlog2bndlem4  20656  pntrlog2bndlem5  20657  gxval  20850  ballotlemsval  22993  ballotlemsv  22994  ballotlemsf1o  22998  ballotlemieq  23001  rdgprc0  23484  dfrdg2  23486  lineval222  25411  lineval3a  25415  sgplpte21  25464  sgplpte22  25470  isray2  25485  isray  25486  aomclem8  26491  pmtrval  26726  pmtrfv  26727  cdleme27b  29687  cdleme29b  29694  cdleme31sn  29699  cdleme31fv  29709  cdleme40v  29788  cdlemk40  30236  dihffval  30550  dihfval  30551  dihval  30552
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-rab 2523  df-v 2742  df-un 3099  df-if 3507
  Copyright terms: Public domain W3C validator