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

Theorem ifbieq12d 3492
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 3488 . 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 3486 . 2  |-  ( ph  ->  if ( ch ,  A ,  B )  =  if ( ch ,  C ,  D )
)
62, 5eqtrd 2285 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 3470
This theorem is referenced by:  csbifg  3498  opeq1  3696  opeq2  3697  riotaeqdv  6191  riotabidv  6192  tz7.44-2  6306  tz7.44-3  6307  boxcutc  6745  unxpdomlem1  6952  oieq1  7111  oieq2  7112  cantnflem1d  7274  cantnflem1  7275  iunfictbso  7625  dfac12lem1  7653  dfac12r  7656  fin23lem12  7841  fin23lem33  7855  ttukeylem3  8022  ttukey2g  8027  xaddval  10428  seqf1olem2  10964  expval  10984  bcval  11195  ccatfval  11305  ccatval1  11308  ccatval2  11309  swrdval  11327  cbvsum  12045  summolem2a  12065  zsum  12068  fsum  12070  sumss  12074  sumss2  12076  fsumcvg2  12077  fsumser  12080  isumless  12178  rpnnen2lem1  12367  rpnnen  12379  ruclem1  12383  sadadd2lem  12524  sadadd2  12525  eucalgval2  12625  pcmpt  12814  pcmptdvds  12816  prmreclem2  12838  prmreclem4  12840  prmreclem5  12841  prmreclem6  12842  prmrec  12843  ramub1lem2  12948  ramcl  12950  ressval  13069  gsumvalx  14286  gsumpropd  14288  gsumress  14289  mulgval  14404  cyggenod2  15007  dmdprdsplitlem  15107  mvrfval  15997  evlslem2  16081  coe1tmmul2fv  16186  coe1pwmulfv  16188  xrsdsval  16247  cyggic  16358  fclsval  17535  ptcmplem3  17580  stdbdmetval  17892  stdbdxmet  17893  xrhmeo  18276  phtpycc  18321  pcovalg  18342  pcocn  18347  pcohtpylem  18349  pcopt2  18353  pcoass  18354  pcorevlem  18356  cmetcaulem  18546  ovolunlem1a  18687  ovolunlem1  18688  ovolicc2lem3  18710  ovolicc2lem4  18711  ovolicc2lem5  18712  ioombl1  18751  mbfmax  18836  mbfpos  18838  mbfposb  18840  i1fres  18892  i1fposd  18894  mbfi1fseqlem2  18903  mbfi1fseq  18908  mbfi1flimlem  18909  mbfi1flim  18910  itg2splitlem  18935  itg2cnlem1  18948  itg2cn  18950  isibl  18952  isibl2  18953  iblitg  18955  dfitg  18956  cbvitg  18962  itgeq2  18964  itgvallem  18971  iblneg  18989  itgneg  18990  itgss3  19001  itgcn  19029  ditgeq1  19030  ditgeq2  19031  deg1suble  19325  ig1pval  19390  elply2  19410  dgrsub  19485  aareccl  19538  cxpval  19879  vmaval  20183  prmorcht  20248  musumsum  20264  muinv  20265  pclogsum  20286  dchrelbasd  20310  dchrptlem2  20336  bposlem5  20359  lgsval  20371  lgsfval  20372  lgsdir  20401  lgsdilem2  20402  lgsdi  20403  lgsne0  20404  rplogsumlem2  20466  pntrlog2bndlem4  20561  pntrlog2bndlem5  20562  gxval  20755  rdgprc0  23318  dfrdg2  23320  lineval222  25245  lineval3a  25249  sgplpte21  25298  sgplpte22  25304  isray2  25319  isray  25320  aomclem8  26325  pmtrval  26560  pmtrfv  26561  cdleme27b  29358  cdleme29b  29365  cdleme31sn  29370  cdleme31fv  29380  cdleme40v  29459  cdlemk40  29907  dihffval  30221  dihfval  30222  dihval  30223
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-rab 2516  df-v 2729  df-un 3083  df-if 3471
  Copyright terms: Public domain W3C validator