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

Theorem ifbieq2d 3585
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 3583 . 2  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ch ,  C ,  A )
)
3 ifbieq2d.2 . . 3  |-  ( ph  ->  A  =  B )
43ifeq2d 3580 . 2  |-  ( ph  ->  if ( ch ,  C ,  A )  =  if ( ch ,  C ,  B )
)
52, 4eqtrd 2315 1  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ch ,  C ,  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623   ifcif 3565
This theorem is referenced by:  tz7.44-2  6420  tz7.44-3  6421  oev  6513  cantnfp1lem1  7380  cantnfp1lem3  7382  fin23lem12  7957  fin23lem33  7971  axcc2  8063  ttukeylem3  8138  ttukey2g  8143  canthp1lem2  8275  canthp1  8276  xnegeq  10534  xaddval  10550  xmulval  10552  expval  11106  sadcp1  12646  smupp1  12671  gcdval  12687  gcdass  12724  iserodd  12888  pcval  12897  vdwlem6  13033  ramub1lem2  13074  ramcl  13076  mulgval  14569  odval  14849  submod  14880  gexval  14889  znval  16489  ptcmplem2  17747  iccpnfhmeo  18443  pcopt  18520  ioombl1  18919  ioorval  18929  uniioombllem6  18943  itg1addlem3  19053  itg2uba  19098  limcfval  19222  limcmpt  19233  limcco  19243  dvcobr  19295  ig1pval  19558  abelthlem9  19816  logtayllem  20006  logtayl  20007  leibpilem2  20237  rlimcnp2  20261  efrlim  20264  muval  20370  lgsval  20539  lgsfval  20540  lgsval2lem  20545  rpvmasum2  20661  padicval  20766  padicabv  20779  gxval  20925  xrge0iifcv  23316  xrge0iifhom  23319  xrge0tmdALT  23327  xrge0tmd  23328  eupath2lem3  23903  eupath2  23904  rdgprc0  24150  dfrdg2  24152  dfrdg4  24488  axlowdimlem15  24584  axlowdim  24589  prodeq1  25306  isconc1  26006  isconc2  26007  isconc3  26008  fdc  26455  heiborlem4  26538  heiborlem6  26540  heiborlem10  26544  irrapxlem4  26910  sgnval  28245  mapdhval  31914  hdmap1fval  31987  hdmap1vallem  31988  hdmap1val  31989  hdmap1cbv  31993
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-un 3157  df-if 3566
  Copyright terms: Public domain W3C validator