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

Theorem ifbieq2d 4450
 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 4447 . 2 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐴))
3 ifbieq2d.2 . . 3 (𝜑𝐴 = 𝐵)
43ifeq2d 4444 . 2 (𝜑 → if(𝜒, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
52, 4eqtrd 2833 1 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ifcif 4425 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-un 3886  df-if 4426 This theorem is referenced by:  tz7.44-2  8028  tz7.44-3  8029  oev  8124  cantnfp1lem1  9127  cantnfp1lem3  9129  fin23lem12  9744  fin23lem33  9758  axcc2  9850  ttukeylem3  9924  ttukey2g  9929  canthp1lem2  10066  canthp1  10067  xnegeq  12590  xaddval  12606  xmulval  12608  expval  13429  cshfn  14145  ofccat  14322  relexpsucnnr  14378  sgnval  14441  sadcp1  15796  smupp1  15821  gcdval  15837  gcdass  15887  lcmval  15928  lcmass  15950  lcmfval  15957  lcmf0val  15958  lcmfpr  15963  iserodd  16164  pcval  16173  vdwlem6  16314  ramub1lem2  16355  ramcl  16357  mulgval  18223  symgextfv  18541  symgfixfo  18562  odfval  18655  odval  18657  submod  18689  gexval  18698  znval  20231  fvmptnn04if  21461  cpmadumatpoly  21495  cayleyhamilton  21502  cayleyhamiltonALT  21503  ptcmplem2  22665  iccpnfhmeo  23557  pcopt  23634  ioombl1  24173  ioorval  24185  uniioombllem6  24199  itg1addlem3  24309  itg2uba  24354  limcfval  24482  limcmpt  24493  limcco  24503  dvcobr  24556  ig1pval  24780  abelthlem9  25042  logtayllem  25257  logtayl  25258  leibpilem2  25534  rlimcnp2  25559  efrlim  25562  igamval  25639  muval  25724  lgsval  25892  lgsfval  25893  lgsval2lem  25898  rpvmasum2  26103  padicval  26208  padicabv  26221  axlowdimlem15  26757  axlowdim  26762  eupth2lem3lem3  28022  eupth2  28031  eucrct2eupth  28037  psgnfzto1stlem  30799  sgnsv  30859  sgnsval  30860  madjusmdetlem2  31193  madjusmdet  31196  xrge0iifcv  31299  xrge0iifhom  31302  xrge0tmd  31310  xrge0tmdALT  31311  signspval  31944  ex-sategoelel  32793  rdgprc0  33163  dfrdg2  33165  dfrdg4  33537  csbrdgg  34762  finxpeq1  34819  finxpreclem3  34826  poimirlem1  35074  poimirlem7  35080  poimirlem10  35083  poimirlem11  35084  itg2addnclem  35124  itg2addnclem3  35126  itg2addnc  35127  fdc  35199  heiborlem4  35268  heiborlem6  35270  heiborlem10  35274  mapdhval  39036  hdmap1fval  39108  hdmap1vallem  39109  hdmap1val  39110  hdmap1cbv  39114  metakunt3  39368  metakunt4  39369  metakunt6  39371  metakunt7  39372  metakunt8  39373  metakunt10  39375  metakunt11  39376  metakunt12  39377  metakunt20  39385  metakunt21  39386  metakunt22  39387  fsuppind  39471  irrapxlem4  39781  clsk1indlem0  40759  clsk1indlem2  40760  clsk1indlem3  40761  clsk1indlem4  40762  clsk1indlem1  40763  dirkerval2  42751  dirkeritg  42759  dirkercncf  42764  fourierdlem29  42793  fourierdlem37  42801  fourierdlem62  42825  fourierdlem79  42842  fourierdlem81  42844  fourierdlem82  42845  fourierdlem92  42855  fourierdlem96  42859  fourierdlem97  42860  fourierdlem98  42861  fourierdlem99  42862  fourierdlem105  42868  fourierdlem108  42871  fourierdlem110  42873  fourierdlem112  42875  fourierdlem113  42876  fouriersw  42888  etransclem24  42915  etransclem25  42916  etransclem31  42922  etransclem35  42926  etransclem37  42928  sge0val  43020  nnfoctbdjlem  43109  nnfoctbdj  43110  ovnval  43195  ovnval2  43199  ovnval2b  43206  hsphoif  43230  hoidmvval  43231  hsphoival  43233  hoidmv1lelem1  43245  hoidmv1lelem2  43246  hoidmv1lelem3  43247  hoidmv1le  43248  ovnhoi  43257  hoidifhspval  43262  hspmbllem2  43281  ovnsubadd2  43300  blenval  44999
 Copyright terms: Public domain W3C validator