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

Theorem ifbieq2d 3702
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 3700 . 2  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ch ,  C ,  A )
)
3 ifbieq2d.2 . . 3  |-  ( ph  ->  A  =  B )
43ifeq2d 3697 . 2  |-  ( ph  ->  if ( ch ,  C ,  A )  =  if ( ch ,  C ,  B )
)
52, 4eqtrd 2419 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 3682
This theorem is referenced by:  tz7.44-2  6601  tz7.44-3  6602  oev  6694  cantnfp1lem1  7567  cantnfp1lem3  7569  fin23lem12  8144  fin23lem33  8158  axcc2  8250  ttukeylem3  8324  ttukey2g  8329  canthp1lem2  8461  canthp1  8462  xnegeq  10725  xaddval  10741  xmulval  10743  expval  11311  sadcp1  12894  smupp1  12919  gcdval  12935  gcdass  12972  iserodd  13136  pcval  13145  vdwlem6  13281  ramub1lem2  13322  ramcl  13324  mulgval  14819  odval  15099  submod  15130  gexval  15139  znval  16739  ptcmplem2  18005  iccpnfhmeo  18841  pcopt  18918  ioombl1  19323  ioorval  19333  uniioombllem6  19347  itg1addlem3  19457  itg2uba  19502  limcfval  19626  limcmpt  19637  limcco  19647  dvcobr  19699  ig1pval  19962  abelthlem9  20223  logtayllem  20417  logtayl  20418  leibpilem2  20648  rlimcnp2  20672  efrlim  20675  muval  20782  lgsval  20951  lgsfval  20952  lgsval2lem  20957  rpvmasum2  21073  padicval  21178  padicabv  21191  eupath2lem3  21549  eupath2  21550  gxval  21694  xrge0iifcv  24124  xrge0iifhom  24127  xrge0tmdOLD  24135  xrge0tmd  24136  igamval  24610  rdgprc0  25174  dfrdg2  25176  dfrdg4  25513  axlowdimlem15  25609  axlowdim  25614  itg2addnclem  25957  itg2addnc  25959  fdc  26140  heiborlem4  26214  heiborlem6  26216  heiborlem10  26220  irrapxlem4  26579  sgnval  27864  mapdhval  31839  hdmap1fval  31912  hdmap1vallem  31913  hdmap1val  31914  hdmap1cbv  31918
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
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 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rab 2658  df-v 2901  df-un 3268  df-if 3683
  Copyright terms: Public domain W3C validator