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

Theorem ifbieq2d 4255
 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 4252 . 2 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐴))
3 ifbieq2d.2 . . 3 (𝜑𝐴 = 𝐵)
43ifeq2d 4249 . 2 (𝜑 → if(𝜒, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
52, 4eqtrd 2794 1 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1632  ifcif 4230 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-un 3720  df-if 4231 This theorem is referenced by:  tz7.44-2  7673  tz7.44-3  7674  oev  7765  cantnfp1lem1  8750  cantnfp1lem3  8752  fin23lem12  9365  fin23lem33  9379  axcc2  9471  ttukeylem3  9545  ttukey2g  9550  canthp1lem2  9687  canthp1  9688  xnegeq  12251  xaddval  12267  xmulval  12269  expval  13076  cshfn  13756  ofccat  13929  relexpsucnnr  13984  sgnval  14047  sadcp1  15399  smupp1  15424  gcdval  15440  gcdass  15486  lcmval  15527  lcmass  15549  lcmfval  15556  lcmf0val  15557  lcmfpr  15562  iserodd  15762  pcval  15771  vdwlem6  15912  ramub1lem2  15953  ramcl  15955  mulgval  17764  symgextfv  18058  symgfixfo  18079  odval  18173  submod  18204  gexval  18213  znval  20105  fvmptnn04if  20876  cpmadumatpoly  20910  cayleyhamilton  20917  cayleyhamiltonALT  20918  ptcmplem2  22078  iccpnfhmeo  22965  pcopt  23042  ioombl1  23550  ioorval  23562  uniioombllem6  23576  itg1addlem3  23684  itg2uba  23729  limcfval  23855  limcmpt  23866  limcco  23876  dvcobr  23928  ig1pval  24151  abelthlem9  24413  logtayllem  24625  logtayl  24626  leibpilem2  24888  rlimcnp2  24913  efrlim  24916  igamval  24993  muval  25078  lgsval  25246  lgsfval  25247  lgsval2lem  25252  rpvmasum2  25421  padicval  25526  padicabv  25539  axlowdimlem15  26056  axlowdim  26061  eupth2lem3lem3  27403  eupth2  27412  eucrct2eupth  27418  sgnsv  30057  sgnsval  30058  psgnfzto1stlem  30180  madjusmdetlem2  30224  madjusmdet  30227  xrge0iifcv  30310  xrge0iifhom  30313  xrge0tmdOLD  30321  xrge0tmd  30322  signspval  30959  rdgprc0  32025  dfrdg2  32027  dfrdg4  32385  csbrdgg  33504  finxpeq1  33552  finxpreclem3  33559  poimirlem1  33741  poimirlem7  33747  poimirlem10  33750  poimirlem11  33751  itg2addnclem  33792  itg2addnclem3  33794  itg2addnc  33795  fdc  33872  heiborlem4  33944  heiborlem6  33946  heiborlem10  33950  mapdhval  37533  hdmap1fval  37606  hdmap1vallem  37607  hdmap1val  37608  hdmap1cbv  37612  irrapxlem4  37909  clsk1indlem0  38859  clsk1indlem2  38860  clsk1indlem3  38861  clsk1indlem4  38862  clsk1indlem1  38863  dirkerval2  40832  dirkeritg  40840  dirkercncf  40845  fourierdlem29  40874  fourierdlem37  40882  fourierdlem62  40906  fourierdlem79  40923  fourierdlem81  40925  fourierdlem82  40926  fourierdlem92  40936  fourierdlem96  40940  fourierdlem97  40941  fourierdlem98  40942  fourierdlem99  40943  fourierdlem105  40949  fourierdlem108  40952  fourierdlem110  40954  fourierdlem112  40956  fourierdlem113  40957  fouriersw  40969  etransclem24  40996  etransclem25  40997  etransclem31  41003  etransclem35  41007  etransclem37  41009  sge0val  41104  nnfoctbdjlem  41193  nnfoctbdj  41194  ovnval  41279  ovnval2  41283  ovnval2b  41290  hsphoif  41314  hoidmvval  41315  hsphoival  41317  hoidmv1lelem1  41329  hoidmv1lelem2  41330  hoidmv1lelem3  41331  hoidmv1le  41332  ovnhoi  41341  hoidifhspval  41346  hspmbllem2  41365  ovnsubadd2  41384  blenval  42893
 Copyright terms: Public domain W3C validator