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

Theorem ifbieq2d 3598
Description: Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypotheses
Ref Expression
ifbieq2d.1  |-  ( ph  ->  ( ps  <->  ch )
)
ifbieq2d.2  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
ifbieq2d  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ch ,  C ,  B )
)

Proof of Theorem ifbieq2d
StepHypRef Expression
1 ifbieq2d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21ifbid 3596 . 2  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ch ,  C ,  A )
)
3 ifbieq2d.2 . . 3  |-  ( ph  ->  A  =  B )
43ifeq2d 3593 . 2  |-  ( ph  ->  if ( ch ,  C ,  A )  =  if ( ch ,  C ,  B )
)
52, 4eqtrd 2328 1  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ch ,  C ,  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   ifcif 3578
This theorem is referenced by:  tz7.44-2  6436  tz7.44-3  6437  oev  6529  cantnfp1lem1  7396  cantnfp1lem3  7398  fin23lem12  7973  fin23lem33  7987  axcc2  8079  ttukeylem3  8154  ttukey2g  8159  canthp1lem2  8291  canthp1  8292  xnegeq  10550  xaddval  10566  xmulval  10568  expval  11122  sadcp1  12662  smupp1  12687  gcdval  12703  gcdass  12740  iserodd  12904  pcval  12913  vdwlem6  13049  ramub1lem2  13090  ramcl  13092  mulgval  14585  odval  14865  submod  14896  gexval  14905  znval  16505  ptcmplem2  17763  iccpnfhmeo  18459  pcopt  18536  ioombl1  18935  ioorval  18945  uniioombllem6  18959  itg1addlem3  19069  itg2uba  19114  limcfval  19238  limcmpt  19249  limcco  19259  dvcobr  19311  ig1pval  19574  abelthlem9  19832  logtayllem  20022  logtayl  20023  leibpilem2  20253  rlimcnp2  20277  efrlim  20280  muval  20386  lgsval  20555  lgsfval  20556  lgsval2lem  20561  rpvmasum2  20677  padicval  20782  padicabv  20795  gxval  20941  xrge0iifcv  23331  xrge0iifhom  23334  xrge0tmdALT  23342  xrge0tmd  23343  eupath2lem3  23918  eupath2  23919  rdgprc0  24221  dfrdg2  24223  dfrdg4  24560  axlowdimlem15  24656  axlowdim  24661  itg2addnclem  25003  itg2addnc  25005  prodeq1  25409  isconc1  26109  isconc2  26110  isconc3  26111  fdc  26558  heiborlem4  26641  heiborlem6  26643  heiborlem10  26647  irrapxlem4  27013  sgnval  28499  mapdhval  32536  hdmap1fval  32609  hdmap1vallem  32610  hdmap1val  32611  hdmap1cbv  32615
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