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  13055  xaddval  13071  xmulval  13073  expval  13898  cshfn  14610  ofccat  14788  relexpsucnnr  14844  sgnval  14907  sadcp1  16270  smupp1  16295  gcdval  16311  gcdass  16363  lcmval  16403  lcmass  16425  lcmfval  16432  lcmf0val  16433  lcmfpr  16438  iserodd  16642  pcval  16651  vdwlem6  16793  ramub1lem2  16834  ramcl  16836  mulgval  18810  symgextfv  19133  symgfixfo  19154  odfval  19247  odval  19249  submod  19281  gexval  19290  znval  20862  fvmptnn04if  22121  cpmadumatpoly  22155  cayleyhamilton  22162  cayleyhamiltonALT  22163  ptcmplem2  23327  iccpnfhmeo  24231  pcopt  24308  ioombl1  24849  ioorval  24861  uniioombllem6  24875  itg1addlem3  24985  itg2uba  25031  limcfval  25159  limcmpt  25170  limcco  25180  dvcobr  25233  ig1pval  25460  abelthlem9  25722  logtayllem  25937  logtayl  25938  leibpilem2  26214  rlimcnp2  26239  efrlim  26242  igamval  26319  muval  26404  lgsval  26572  lgsfval  26573  lgsval2lem  26578  rpvmasum2  26783  padicval  26888  padicabv  26901  axlowdimlem15  27704  axlowdim  27709  eupth2lem3lem3  28973  eupth2  28982  eucrct2eupth  28988  psgnfzto1stlem  31744  sgnsv  31804  sgnsval  31805  madjusmdetlem2  32183  madjusmdet  32186  xrge0iifcv  32289  xrge0iifhom  32292  xrge0tmd  32300  xrge0tmdALT  32301  signspval  32938  ex-sategoelel  33789  rdgprc0  34159  dfrdg2  34161  dfrdg4  34432  csbrdgg  35696  finxpeq1  35753  finxpreclem3  35760  poimirlem1  35975  poimirlem7  35981  poimirlem10  35984  poimirlem11  35985  itg2addnclem  36025  itg2addnclem3  36027  itg2addnc  36028  fdc  36100  heiborlem4  36169  heiborlem6  36171  heiborlem10  36175  mapdhval  40083  hdmap1fval  40155  hdmap1vallem  40156  hdmap1val  40157  hdmap1cbv  40161  sticksstones10  40459  sticksstones12a  40461  metakunt3  40475  metakunt4  40476  metakunt6  40478  metakunt7  40479  metakunt8  40480  metakunt10  40482  metakunt11  40483  metakunt12  40484  metakunt20  40492  metakunt21  40493  metakunt22  40494  fsuppind  40634  irrapxlem4  41014  clsk1indlem0  42078  clsk1indlem2  42079  clsk1indlem3  42080  clsk1indlem4  42081  clsk1indlem1  42082  dirkerval2  44090  dirkeritg  44098  dirkercncf  44103  fourierdlem29  44132  fourierdlem37  44140  fourierdlem62  44164  fourierdlem79  44181  fourierdlem81  44183  fourierdlem82  44184  fourierdlem92  44194  fourierdlem96  44198  fourierdlem97  44199  fourierdlem98  44200  fourierdlem99  44201  fourierdlem105  44207  fourierdlem108  44210  fourierdlem110  44212  fourierdlem112  44214  fourierdlem113  44215  fouriersw  44227  etransclem24  44254  etransclem25  44255  etransclem31  44261  etransclem35  44265  etransclem37  44267  sge0val  44362  nnfoctbdjlem  44451  nnfoctbdj  44452  ovnval  44537  ovnval2  44541  ovnval2b  44548  hsphoif  44572  hoidmvval  44573  hsphoival  44575  hoidmv1lelem1  44587  hoidmv1lelem2  44588  hoidmv1lelem3  44589  hoidmv1le  44590  ovnhoi  44599  hoidifhspval  44604  hspmbllem2  44623  ovnsubadd2  44642  blenval  46412
  Copyright terms: Public domain W3C validator