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

Theorem ifbieq2d 4511
Description: Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypotheses
Ref Expression
ifbieq2d.1 (𝜑 → (𝜓𝜒))
ifbieq2d.2 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
ifbieq2d (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))

Proof of Theorem ifbieq2d
StepHypRef Expression
1 ifbieq2d.1 . . 3 (𝜑 → (𝜓𝜒))
21ifbid 4508 . 2 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐴))
3 ifbieq2d.2 . . 3 (𝜑𝐴 = 𝐵)
43ifeq2d 4505 . 2 (𝜑 → if(𝜒, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
52, 4eqtrd 2778 1 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  ifcif 4485
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3407  df-v 3446  df-un 3914  df-if 4486
This theorem is referenced by:  tz7.44-2  8321  tz7.44-3  8322  oev  8428  cantnfp1lem1  9548  cantnfp1lem3  9550  ttrclselem2  9596  fin23lem12  10201  fin23lem33  10215  axcc2  10307  ttukeylem3  10381  ttukey2g  10386  canthp1lem2  10523  canthp1  10524  xnegeq  13056  xaddval  13072  xmulval  13074  expval  13899  cshfn  14611  ofccat  14789  relexpsucnnr  14845  sgnval  14908  sadcp1  16271  smupp1  16296  gcdval  16312  gcdass  16364  lcmval  16404  lcmass  16426  lcmfval  16433  lcmf0val  16434  lcmfpr  16439  iserodd  16643  pcval  16652  vdwlem6  16794  ramub1lem2  16835  ramcl  16837  mulgval  18811  symgextfv  19135  symgfixfo  19156  odfval  19249  odval  19251  submod  19286  gexval  19295  znval  20867  fvmptnn04if  22126  cpmadumatpoly  22160  cayleyhamilton  22167  cayleyhamiltonALT  22168  ptcmplem2  23332  iccpnfhmeo  24236  pcopt  24313  ioombl1  24854  ioorval  24866  uniioombllem6  24880  itg1addlem3  24990  itg2uba  25036  limcfval  25164  limcmpt  25175  limcco  25185  dvcobr  25238  ig1pval  25465  abelthlem9  25727  logtayllem  25942  logtayl  25943  leibpilem2  26219  rlimcnp2  26244  efrlim  26247  igamval  26324  muval  26409  lgsval  26577  lgsfval  26578  lgsval2lem  26583  rpvmasum2  26788  padicval  26893  padicabv  26906  axlowdimlem15  27710  axlowdim  27715  eupth2lem3lem3  28979  eupth2  28988  eucrct2eupth  28994  psgnfzto1stlem  31750  sgnsv  31810  sgnsval  31811  madjusmdetlem2  32189  madjusmdet  32192  xrge0iifcv  32295  xrge0iifhom  32298  xrge0tmd  32306  xrge0tmdALT  32307  signspval  32944  ex-sategoelel  33795  rdgprc0  34162  dfrdg2  34164  dfrdg4  34467  csbrdgg  35731  finxpeq1  35788  finxpreclem3  35795  poimirlem1  36010  poimirlem7  36016  poimirlem10  36019  poimirlem11  36020  itg2addnclem  36060  itg2addnclem3  36062  itg2addnc  36063  fdc  36135  heiborlem4  36204  heiborlem6  36206  heiborlem10  36210  mapdhval  40118  hdmap1fval  40190  hdmap1vallem  40191  hdmap1val  40192  hdmap1cbv  40196  sticksstones10  40494  sticksstones12a  40496  metakunt3  40510  metakunt4  40511  metakunt6  40513  metakunt7  40514  metakunt8  40515  metakunt10  40517  metakunt11  40518  metakunt12  40519  metakunt20  40527  metakunt21  40528  metakunt22  40529  fsuppind  40667  irrapxlem4  41050  clsk1indlem0  42114  clsk1indlem2  42115  clsk1indlem3  42116  clsk1indlem4  42117  clsk1indlem1  42118  dirkerval2  44126  dirkeritg  44134  dirkercncf  44139  fourierdlem29  44168  fourierdlem37  44176  fourierdlem62  44200  fourierdlem79  44217  fourierdlem81  44219  fourierdlem82  44220  fourierdlem92  44230  fourierdlem96  44234  fourierdlem97  44235  fourierdlem98  44236  fourierdlem99  44237  fourierdlem105  44243  fourierdlem108  44246  fourierdlem110  44248  fourierdlem112  44250  fourierdlem113  44251  fouriersw  44263  etransclem24  44290  etransclem25  44291  etransclem31  44297  etransclem35  44301  etransclem37  44303  sge0val  44398  nnfoctbdjlem  44487  nnfoctbdj  44488  ovnval  44573  ovnval2  44577  ovnval2b  44584  hsphoif  44608  hoidmvval  44609  hsphoival  44611  hoidmv1lelem1  44623  hoidmv1lelem2  44624  hoidmv1lelem3  44625  hoidmv1le  44626  ovnhoi  44635  hoidifhspval  44640  hspmbllem2  44659  ovnsubadd2  44678  blenval  46448
  Copyright terms: Public domain W3C validator