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

Theorem ifbieq12d 3721
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 3717 . 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 3715 . 2  |-  ( ph  ->  if ( ch ,  A ,  B )  =  if ( ch ,  C ,  D )
)
62, 5eqtrd 2436 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  C ,  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   ifcif 3699
This theorem is referenced by:  csbifg  3727  opeq1  3944  opeq2  3945  riotaeqdv  6509  riotabidv  6510  tz7.44-2  6624  tz7.44-3  6625  boxcutc  7064  unxpdomlem1  7272  oieq1  7437  oieq2  7438  cantnflem1d  7600  cantnflem1  7601  iunfictbso  7951  dfac12lem1  7979  dfac12r  7982  fin23lem12  8167  fin23lem33  8181  ttukeylem3  8347  ttukey2g  8352  xaddval  10765  seqf1olem2  11318  expval  11339  bcval  11550  ccatfval  11697  ccatval1  11700  ccatval2  11701  swrdval  11719  cbvsum  12444  summolem2a  12464  zsum  12467  fsum  12469  sumss  12473  sumss2  12475  fsumcvg2  12476  fsumser  12479  isumless  12580  rpnnen2lem1  12769  rpnnen  12781  ruclem1  12785  sadadd2lem  12926  sadadd2  12927  eucalgval2  13027  pcmpt  13216  pcmptdvds  13218  prmreclem2  13240  prmreclem4  13242  prmreclem5  13243  prmreclem6  13244  prmrec  13245  ramub1lem2  13350  ramcl  13352  ressval  13471  gsumvalx  14729  gsumpropd  14731  gsumress  14732  mulgval  14847  cyggenod2  15450  dmdprdsplitlem  15550  mvrfval  16439  evlslem2  16523  coe1tmmul2fv  16625  coe1pwmulfv  16627  xrsdsval  16697  cyggic  16808  fclsval  17993  ptcmplem3  18038  stdbdmetval  18497  stdbdxmet  18498  xrhmeo  18924  phtpycc  18969  pcovalg  18990  pcocn  18995  pcohtpylem  18997  pcopt2  19001  pcoass  19002  pcorevlem  19004  cmetcaulem  19194  ovolunlem1a  19345  ovolunlem1  19346  ovolicc2lem3  19368  ovolicc2lem4  19369  ovolicc2lem5  19370  ioombl1  19409  mbfmax  19494  mbfpos  19496  mbfposb  19498  i1fres  19550  i1fposd  19552  mbfi1fseqlem2  19561  mbfi1fseq  19566  mbfi1flimlem  19567  mbfi1flim  19568  itg2splitlem  19593  itg2cnlem1  19606  itg2cn  19608  isibl  19610  isibl2  19611  iblitg  19613  dfitg  19614  cbvitg  19620  itgeq2  19622  itgvallem  19629  iblneg  19647  itgneg  19648  itgss3  19659  itgcn  19687  ditgeq1  19688  ditgeq2  19689  deg1suble  19983  ig1pval  20048  elply2  20068  dgrsub  20143  aareccl  20196  cxpval  20508  vmaval  20849  prmorcht  20914  musumsum  20930  muinv  20931  pclogsum  20952  dchrelbasd  20976  dchrptlem2  21002  bposlem5  21025  lgsval  21037  lgsfval  21038  lgsdir  21067  lgsdilem2  21068  lgsdi  21069  lgsne0  21070  rplogsumlem2  21132  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  gxval  21799  gsumpropd2lem  24173  ballotlemsval  24719  ballotlemsv  24720  ballotlemsf1o  24724  ballotlemieq  24727  lgamgulmlem4  24769  lgamgulmlem5  24770  cbvprod  25194  prodmolem2a  25213  zprod  25216  fprod  25220  fprodntriv  25221  prodss  25226  rdgprc0  25364  dfrdg2  25366  mblfinlem  26143  itg2addnclem  26155  itg2addnclem3  26157  itgaddnclem2  26163  aomclem8  27027  pmtrval  27262  pmtrfv  27263  afveq12d  27864  cdleme27b  30850  cdleme29b  30857  cdleme31sn  30862  cdleme31fv  30872  cdleme40v  30951  cdlemk40  31399  dihffval  31713  dihfval  31714  dihval  31715
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-un 3285  df-if 3700
  Copyright terms: Public domain W3C validator