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

Theorem ifbieq12d 3600
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 3596 . 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 3594 . 2  |-  ( ph  ->  if ( ch ,  A ,  B )  =  if ( ch ,  C ,  D )
)
62, 5eqtrd 2328 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  C ,  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   ifcif 3578
This theorem is referenced by:  csbifg  3606  opeq1  3812  opeq2  3813  riotaeqdv  6321  riotabidv  6322  tz7.44-2  6436  tz7.44-3  6437  boxcutc  6875  unxpdomlem1  7083  oieq1  7243  oieq2  7244  cantnflem1d  7406  cantnflem1  7407  iunfictbso  7757  dfac12lem1  7785  dfac12r  7788  fin23lem12  7973  fin23lem33  7987  ttukeylem3  8154  ttukey2g  8159  xaddval  10566  seqf1olem2  11102  expval  11122  bcval  11333  ccatfval  11444  ccatval1  11447  ccatval2  11448  swrdval  11466  cbvsum  12184  summolem2a  12204  zsum  12207  fsum  12209  sumss  12213  sumss2  12215  fsumcvg2  12216  fsumser  12219  isumless  12320  rpnnen2lem1  12509  rpnnen  12521  ruclem1  12525  sadadd2lem  12666  sadadd2  12667  eucalgval2  12767  pcmpt  12956  pcmptdvds  12958  prmreclem2  12980  prmreclem4  12982  prmreclem5  12983  prmreclem6  12984  prmrec  12985  ramub1lem2  13090  ramcl  13092  ressval  13211  gsumvalx  14467  gsumpropd  14469  gsumress  14470  mulgval  14585  cyggenod2  15188  dmdprdsplitlem  15288  mvrfval  16181  evlslem2  16265  coe1tmmul2fv  16370  coe1pwmulfv  16372  xrsdsval  16431  cyggic  16542  fclsval  17719  ptcmplem3  17764  stdbdmetval  18076  stdbdxmet  18077  xrhmeo  18460  phtpycc  18505  pcovalg  18526  pcocn  18531  pcohtpylem  18533  pcopt2  18537  pcoass  18538  pcorevlem  18540  cmetcaulem  18730  ovolunlem1a  18871  ovolunlem1  18872  ovolicc2lem3  18894  ovolicc2lem4  18895  ovolicc2lem5  18896  ioombl1  18935  mbfmax  19020  mbfpos  19022  mbfposb  19024  i1fres  19076  i1fposd  19078  mbfi1fseqlem2  19087  mbfi1fseq  19092  mbfi1flimlem  19093  mbfi1flim  19094  itg2splitlem  19119  itg2cnlem1  19132  itg2cn  19134  isibl  19136  isibl2  19137  iblitg  19139  dfitg  19140  cbvitg  19146  itgeq2  19148  itgvallem  19155  iblneg  19173  itgneg  19174  itgss3  19185  itgcn  19213  ditgeq1  19214  ditgeq2  19215  deg1suble  19509  ig1pval  19574  elply2  19594  dgrsub  19669  aareccl  19722  cxpval  20027  vmaval  20367  prmorcht  20432  musumsum  20448  muinv  20449  pclogsum  20470  dchrelbasd  20494  dchrptlem2  20520  bposlem5  20543  lgsval  20555  lgsfval  20556  lgsdir  20585  lgsdilem2  20586  lgsdi  20587  lgsne0  20588  rplogsumlem2  20650  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  gxval  20941  ballotlemsval  23083  ballotlemsv  23084  ballotlemsf1o  23088  ballotlemieq  23091  gsumpropd2lem  23394  itgmeq123dTMP  23604  cbvcprod  24137  prodmolem2a  24157  zprod  24160  fprod  24164  rdgprc0  24221  dfrdg2  24223  itg2addnclem  25003  itg2addnc  25005  itgaddnclem2  25010  lineval222  26182  lineval3a  26186  sgplpte21  26235  sgplpte22  26241  isray2  26256  isray  26257  aomclem8  27262  pmtrval  27497  pmtrfv  27498  afveq12d  28101  cdleme27b  31179  cdleme29b  31186  cdleme31sn  31191  cdleme31fv  31201  cdleme40v  31280  cdlemk40  31728  dihffval  32042  dihfval  32043  dihval  32044
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-un 3170  df-if 3579
  Copyright terms: Public domain W3C validator