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

Theorem ifbieq2d 4083
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 4080 . 2 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐴))
3 ifbieq2d.2 . . 3 (𝜑𝐴 = 𝐵)
43ifeq2d 4077 . 2 (𝜑 → if(𝜒, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
52, 4eqtrd 2655 1 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  ifcif 4058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3188  df-un 3560  df-if 4059
This theorem is referenced by:  tz7.44-2  7448  tz7.44-3  7449  oev  7539  cantnfp1lem1  8519  cantnfp1lem3  8521  fin23lem12  9097  fin23lem33  9111  axcc2  9203  ttukeylem3  9277  ttukey2g  9282  canthp1lem2  9419  canthp1  9420  xnegeq  11981  xaddval  11997  xmulval  11999  expval  12802  cshfn  13473  ofccat  13642  relexpsucnnr  13699  sgnval  13762  sadcp1  15101  smupp1  15126  gcdval  15142  gcdass  15188  lcmval  15229  lcmass  15251  lcmfval  15258  lcmf0val  15259  lcmfpr  15264  iserodd  15464  pcval  15473  vdwlem6  15614  ramub1lem2  15655  ramcl  15657  mulgval  17464  symgextfv  17759  symgfixfo  17780  odval  17874  submod  17905  gexval  17914  znval  19802  fvmptnn04if  20573  cpmadumatpoly  20607  cayleyhamilton  20614  cayleyhamiltonALT  20615  ptcmplem2  21767  iccpnfhmeo  22652  pcopt  22730  ioombl1  23237  ioorval  23248  uniioombllem6  23262  itg1addlem3  23371  itg2uba  23416  limcfval  23542  limcmpt  23553  limcco  23563  dvcobr  23615  ig1pval  23836  abelthlem9  24098  logtayllem  24305  logtayl  24306  leibpilem2  24568  rlimcnp2  24593  efrlim  24596  igamval  24673  muval  24758  lgsval  24926  lgsfval  24927  lgsval2lem  24932  rpvmasum2  25101  padicval  25206  padicabv  25219  axlowdimlem15  25736  axlowdim  25741  eupth2lem3lem3  26956  eupth2  26965  eucrct2eupth  26971  sgnsv  29512  sgnsval  29513  psgnfzto1stlem  29635  madjusmdetlem2  29676  madjusmdet  29679  xrge0iifcv  29762  xrge0iifhom  29765  xrge0tmdOLD  29773  xrge0tmd  29774  signspval  30409  rdgprc0  31400  dfrdg2  31402  dfrdg4  31700  csbrdgg  32807  finxpeq1  32855  finxpreclem3  32862  poimirlem1  33042  poimirlem7  33048  poimirlem10  33051  poimirlem11  33052  itg2addnclem  33093  itg2addnclem3  33095  itg2addnc  33096  fdc  33173  heiborlem4  33245  heiborlem6  33247  heiborlem10  33251  mapdhval  36493  hdmap1fval  36566  hdmap1vallem  36567  hdmap1val  36568  hdmap1cbv  36572  irrapxlem4  36869  clsk1indlem0  37821  clsk1indlem2  37822  clsk1indlem3  37823  clsk1indlem4  37824  clsk1indlem1  37825  dirkerval2  39618  dirkeritg  39626  dirkercncf  39631  fourierdlem29  39660  fourierdlem37  39668  fourierdlem62  39692  fourierdlem79  39709  fourierdlem81  39711  fourierdlem82  39712  fourierdlem92  39722  fourierdlem96  39726  fourierdlem97  39727  fourierdlem98  39728  fourierdlem99  39729  fourierdlem105  39735  fourierdlem108  39738  fourierdlem110  39740  fourierdlem112  39742  fourierdlem113  39743  fouriersw  39755  etransclem24  39782  etransclem25  39783  etransclem31  39789  etransclem35  39793  etransclem37  39795  sge0val  39890  nnfoctbdjlem  39979  nnfoctbdj  39980  ovnval  40062  ovnval2  40066  ovnval2b  40073  hsphoif  40097  hoidmvval  40098  hsphoival  40100  hoidmv1lelem1  40112  hoidmv1lelem2  40113  hoidmv1lelem3  40114  hoidmv1le  40115  ovnhoi  40124  hoidifhspval  40129  hspmbllem2  40148  ovnsubadd2  40167  blenval  41657
  Copyright terms: Public domain W3C validator