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

Theorem ifbieq2d 4490
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 4487 . 2 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐴))
3 ifbieq2d.2 . . 3 (𝜑𝐴 = 𝐵)
43ifeq2d 4484 . 2 (𝜑 → if(𝜒, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
52, 4eqtrd 2856 1 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  ifcif 4465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-un 3940  df-if 4466
This theorem is referenced by:  tz7.44-2  8034  tz7.44-3  8035  oev  8130  cantnfp1lem1  9130  cantnfp1lem3  9132  fin23lem12  9742  fin23lem33  9756  axcc2  9848  ttukeylem3  9922  ttukey2g  9927  canthp1lem2  10064  canthp1  10065  xnegeq  12590  xaddval  12606  xmulval  12608  expval  13421  cshfn  14142  ofccat  14319  relexpsucnnr  14374  sgnval  14437  sadcp1  15794  smupp1  15819  gcdval  15835  gcdass  15885  lcmval  15926  lcmass  15948  lcmfval  15955  lcmf0val  15956  lcmfpr  15961  iserodd  16162  pcval  16171  vdwlem6  16312  ramub1lem2  16353  ramcl  16355  mulgval  18168  symgextfv  18477  symgfixfo  18498  odfval  18591  odval  18593  submod  18625  gexval  18634  znval  20612  fvmptnn04if  21387  cpmadumatpoly  21421  cayleyhamilton  21428  cayleyhamiltonALT  21429  ptcmplem2  22591  iccpnfhmeo  23478  pcopt  23555  ioombl1  24092  ioorval  24104  uniioombllem6  24118  itg1addlem3  24228  itg2uba  24273  limcfval  24399  limcmpt  24410  limcco  24420  dvcobr  24472  ig1pval  24695  abelthlem9  24957  logtayllem  25169  logtayl  25170  leibpilem2  25447  rlimcnp2  25472  efrlim  25475  igamval  25552  muval  25637  lgsval  25805  lgsfval  25806  lgsval2lem  25811  rpvmasum2  26016  padicval  26121  padicabv  26134  axlowdimlem15  26670  axlowdim  26675  eupth2lem3lem3  27937  eupth2  27946  eucrct2eupth  27952  psgnfzto1stlem  30670  sgnsv  30730  sgnsval  30731  madjusmdetlem2  30993  madjusmdet  30996  xrge0iifcv  31077  xrge0iifhom  31080  xrge0tmd  31088  xrge0tmdALT  31089  signspval  31722  ex-sategoelel  32566  rdgprc0  32936  dfrdg2  32938  dfrdg4  33310  csbrdgg  34493  finxpeq1  34550  finxpreclem3  34557  poimirlem1  34775  poimirlem7  34781  poimirlem10  34784  poimirlem11  34785  itg2addnclem  34825  itg2addnclem3  34827  itg2addnc  34828  fdc  34903  heiborlem4  34975  heiborlem6  34977  heiborlem10  34981  mapdhval  38742  hdmap1fval  38814  hdmap1vallem  38815  hdmap1val  38816  hdmap1cbv  38820  irrapxlem4  39302  clsk1indlem0  40271  clsk1indlem2  40272  clsk1indlem3  40273  clsk1indlem4  40274  clsk1indlem1  40275  dirkerval2  42260  dirkeritg  42268  dirkercncf  42273  fourierdlem29  42302  fourierdlem37  42310  fourierdlem62  42334  fourierdlem79  42351  fourierdlem81  42353  fourierdlem82  42354  fourierdlem92  42364  fourierdlem96  42368  fourierdlem97  42369  fourierdlem98  42370  fourierdlem99  42371  fourierdlem105  42377  fourierdlem108  42380  fourierdlem110  42382  fourierdlem112  42384  fourierdlem113  42385  fouriersw  42397  etransclem24  42424  etransclem25  42425  etransclem31  42431  etransclem35  42435  etransclem37  42437  sge0val  42529  nnfoctbdjlem  42618  nnfoctbdj  42619  ovnval  42704  ovnval2  42708  ovnval2b  42715  hsphoif  42739  hoidmvval  42740  hsphoival  42742  hoidmv1lelem1  42754  hoidmv1lelem2  42755  hoidmv1lelem3  42756  hoidmv1le  42757  ovnhoi  42766  hoidifhspval  42771  hspmbllem2  42790  ovnsubadd2  42809  blenval  44529
  Copyright terms: Public domain W3C validator