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

Theorem ifbieq2d 3751
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 3749 . 2  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ch ,  C ,  A )
)
3 ifbieq2d.2 . . 3  |-  ( ph  ->  A  =  B )
43ifeq2d 3746 . 2  |-  ( ph  ->  if ( ch ,  C ,  A )  =  if ( ch ,  C ,  B )
)
52, 4eqtrd 2467 1  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ch ,  C ,  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652   ifcif 3731
This theorem is referenced by:  tz7.44-2  6657  tz7.44-3  6658  oev  6750  cantnfp1lem1  7626  cantnfp1lem3  7628  fin23lem12  8203  fin23lem33  8217  axcc2  8309  ttukeylem3  8383  ttukey2g  8388  canthp1lem2  8520  canthp1  8521  xnegeq  10785  xaddval  10801  xmulval  10803  expval  11376  sadcp1  12959  smupp1  12984  gcdval  13000  gcdass  13037  iserodd  13201  pcval  13210  vdwlem6  13346  ramub1lem2  13387  ramcl  13389  mulgval  14884  odval  15164  submod  15195  gexval  15204  znval  16808  ptcmplem2  18076  iccpnfhmeo  18962  pcopt  19039  ioombl1  19448  ioorval  19458  uniioombllem6  19472  itg1addlem3  19582  itg2uba  19627  limcfval  19751  limcmpt  19762  limcco  19772  dvcobr  19824  ig1pval  20087  abelthlem9  20348  logtayllem  20542  logtayl  20543  leibpilem2  20773  rlimcnp2  20797  efrlim  20800  muval  20907  lgsval  21076  lgsfval  21077  lgsval2lem  21082  rpvmasum2  21198  padicval  21303  padicabv  21316  eupath2lem3  21693  eupath2  21694  gxval  21838  xrge0iifcv  24312  xrge0iifhom  24315  xrge0tmdOLD  24323  xrge0tmd  24324  igamval  24823  rdgprc0  25413  dfrdg2  25415  dfrdg4  25787  axlowdimlem15  25887  axlowdim  25892  itg2addnclem  26246  itg2addnclem3  26248  itg2addnc  26249  fdc  26440  heiborlem4  26514  heiborlem6  26516  heiborlem10  26520  irrapxlem4  26879  sgnval  28455  mapdhval  32459  hdmap1fval  32532  hdmap1vallem  32533  hdmap1val  32534  hdmap1cbv  32538
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-un 3317  df-if 3732
  Copyright terms: Public domain W3C validator