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

Theorem ifbieq12d 3547
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 3543 . 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 3541 . 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 3525
This theorem is referenced by:  csbifg  3553  opeq1  3756  opeq2  3757  riotaeqdv  6259  riotabidv  6260  tz7.44-2  6374  tz7.44-3  6375  boxcutc  6813  unxpdomlem1  7021  oieq1  7181  oieq2  7182  cantnflem1d  7344  cantnflem1  7345  iunfictbso  7695  dfac12lem1  7723  dfac12r  7726  fin23lem12  7911  fin23lem33  7925  ttukeylem3  8092  ttukey2g  8097  xaddval  10502  seqf1olem2  11038  expval  11058  bcval  11269  ccatfval  11379  ccatval1  11382  ccatval2  11383  swrdval  11401  cbvsum  12119  summolem2a  12139  zsum  12142  fsum  12144  sumss  12148  sumss2  12150  fsumcvg2  12151  fsumser  12154  isumless  12252  rpnnen2lem1  12441  rpnnen  12453  ruclem1  12457  sadadd2lem  12598  sadadd2  12599  eucalgval2  12699  pcmpt  12888  pcmptdvds  12890  prmreclem2  12912  prmreclem4  12914  prmreclem5  12915  prmreclem6  12916  prmrec  12917  ramub1lem2  13022  ramcl  13024  ressval  13143  gsumvalx  14399  gsumpropd  14401  gsumress  14402  mulgval  14517  cyggenod2  15120  dmdprdsplitlem  15220  mvrfval  16113  evlslem2  16197  coe1tmmul2fv  16302  coe1pwmulfv  16304  xrsdsval  16363  cyggic  16474  fclsval  17651  ptcmplem3  17696  stdbdmetval  18008  stdbdxmet  18009  xrhmeo  18392  phtpycc  18437  pcovalg  18458  pcocn  18463  pcohtpylem  18465  pcopt2  18469  pcoass  18470  pcorevlem  18472  cmetcaulem  18662  ovolunlem1a  18803  ovolunlem1  18804  ovolicc2lem3  18826  ovolicc2lem4  18827  ovolicc2lem5  18828  ioombl1  18867  mbfmax  18952  mbfpos  18954  mbfposb  18956  i1fres  19008  i1fposd  19010  mbfi1fseqlem2  19019  mbfi1fseq  19024  mbfi1flimlem  19025  mbfi1flim  19026  itg2splitlem  19051  itg2cnlem1  19064  itg2cn  19066  isibl  19068  isibl2  19069  iblitg  19071  dfitg  19072  cbvitg  19078  itgeq2  19080  itgvallem  19087  iblneg  19105  itgneg  19106  itgss3  19117  itgcn  19145  ditgeq1  19146  ditgeq2  19147  deg1suble  19441  ig1pval  19506  elply2  19526  dgrsub  19601  aareccl  19654  cxpval  19959  vmaval  20299  prmorcht  20364  musumsum  20380  muinv  20381  pclogsum  20402  dchrelbasd  20426  dchrptlem2  20452  bposlem5  20475  lgsval  20487  lgsfval  20488  lgsdir  20517  lgsdilem2  20518  lgsdi  20519  lgsne0  20520  rplogsumlem2  20582  pntrlog2bndlem4  20677  pntrlog2bndlem5  20678  gxval  20871  ballotlemsval  23014  ballotlemsv  23015  ballotlemsf1o  23019  ballotlemieq  23022  rdgprc0  23505  dfrdg2  23507  lineval222  25432  lineval3a  25436  sgplpte21  25485  sgplpte22  25491  isray2  25506  isray  25507  aomclem8  26512  pmtrval  26747  pmtrfv  26748  cdleme27b  29708  cdleme29b  29715  cdleme31sn  29720  cdleme31fv  29730  cdleme40v  29809  cdlemk40  30257  dihffval  30571  dihfval  30572  dihval  30573
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 2525  df-v 2759  df-un 3118  df-if 3526
  Copyright terms: Public domain W3C validator