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

Theorem ifbieq2d 3719
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 3717 . 2  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ch ,  C ,  A )
)
3 ifbieq2d.2 . . 3  |-  ( ph  ->  A  =  B )
43ifeq2d 3714 . 2  |-  ( ph  ->  if ( ch ,  C ,  A )  =  if ( ch ,  C ,  B )
)
52, 4eqtrd 2436 1  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ch ,  C ,  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   ifcif 3699
This theorem is referenced by:  tz7.44-2  6624  tz7.44-3  6625  oev  6717  cantnfp1lem1  7590  cantnfp1lem3  7592  fin23lem12  8167  fin23lem33  8181  axcc2  8273  ttukeylem3  8347  ttukey2g  8352  canthp1lem2  8484  canthp1  8485  xnegeq  10749  xaddval  10765  xmulval  10767  expval  11339  sadcp1  12922  smupp1  12947  gcdval  12963  gcdass  13000  iserodd  13164  pcval  13173  vdwlem6  13309  ramub1lem2  13350  ramcl  13352  mulgval  14847  odval  15127  submod  15158  gexval  15167  znval  16771  ptcmplem2  18037  iccpnfhmeo  18923  pcopt  19000  ioombl1  19409  ioorval  19419  uniioombllem6  19433  itg1addlem3  19543  itg2uba  19588  limcfval  19712  limcmpt  19723  limcco  19733  dvcobr  19785  ig1pval  20048  abelthlem9  20309  logtayllem  20503  logtayl  20504  leibpilem2  20734  rlimcnp2  20758  efrlim  20761  muval  20868  lgsval  21037  lgsfval  21038  lgsval2lem  21043  rpvmasum2  21159  padicval  21264  padicabv  21277  eupath2lem3  21654  eupath2  21655  gxval  21799  xrge0iifcv  24273  xrge0iifhom  24276  xrge0tmdOLD  24284  xrge0tmd  24285  igamval  24784  rdgprc0  25364  dfrdg2  25366  dfrdg4  25703  axlowdimlem15  25799  axlowdim  25804  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  fdc  26339  heiborlem4  26413  heiborlem6  26415  heiborlem10  26419  irrapxlem4  26778  sgnval  28232  mapdhval  32207  hdmap1fval  32280  hdmap1vallem  32281  hdmap1val  32282  hdmap1cbv  32286
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