Theorem iffalsed 4487

Description: Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

Ref	Expression
iffalsed.1	⊢ (𝜑 → ¬ 𝜒)

Assertion

Ref	Expression
iffalsed	⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐵)

Proof of Theorem iffalsed

Step	Hyp	Ref	Expression
1		iffalsed.1	. 2 ⊢ (𝜑 → ¬ 𝜒)
2		iffalse 4485	. 2 ⊢ (¬ 𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541  ifcif 4476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-if 4477

This theorem is referenced by:  ifeqor  4528  ifnot  4529  ifan  4530  somincom  6087  partfun  6635  mpodifsnif  7469  tz7.44-2  8334  tz7.44-3  8335  unxpdomlem2  9150  sniffsupp  9293  unwdomg  9479  cantnfp1lem1  9577  cantnfp1lem3  9579  cantnflem1d  9587  ttrcltr  9615  updjudhcoinrg  9835  ttukeylem7  10415  canthp1lem2  10553  pwfseqlem3  10560  xmulneg1  13172  rexmul  13174  xmulpnf1  13177  fzprval  13489  expnnval  13975  expneg  13980  tpf1ofv1  14408  tpf1ofv2  14409  ccatval2  14489  ccatalpha  14505  swrdnd  14566  swrdnd2  14567  swrd0  14570  swrdccatin2  14640  relexpsucnnr  14936  relexp1g  14937  sgnp  15001  sgnn  15005  absmax  15241  sumss2  15637  fsumsplit  15652  fprodntriv  15853  fprodsplit  15877  ef0lem  15989  rpnnen2lem9  16135  sadadd2  16375  eucalgf  16498  eucalginv  16499  eucalglt  16500  iserodd  16751  pcmpt  16808  pcmpt2  16809  ramtub  16928  prmo1  16953  fvprif  17469  gsumval2a  18597  mgm2nsgrplem2  18831  mgm2nsgrplem3  18832  sgrp2nmndlem3  18837  mulgnn  18992  mulgnegnn  19001  symgextfv  19334  pmtrprfv3  19370  pmtrdifellem4  19395  pmtrprfval  19403  pmtrprfvalrn  19404  odlem2  19455  dfod2  19480  gsumval3a  19819  gsumzsplit  19843  dmdprdsplitlem  19955  ablsimpgfind  20028  abvtrivd  20751  uvcvv0  21731  uvcff  21732  psrlidm  21902  psrridm  21903  mvrcl  21932  mplmon  21973  mplmonmul  21974  mplcoe1  21975  mplcoe5  21978  evlslem3  22018  coe1tmfv2  22192  cply1coe0  22219  cply1coe0bi  22220  gsummoncoe1  22226  mulmarep1gsum1  22491  1marepvsma1  22501  mdetunilem2  22531  mdetunilem9  22538  maducoeval2  22558  symgmatr01lem  22571  gsummatr01lem3  22575  gsummatr01lem4  22576  gsummatr01  22577  m2cpm  22659  m2cpminvid2lem  22672  pmatcollpw3fi1lem1  22704  mp2pm2mplem4  22727  chfacffsupp  22774  chfacfscmul0  22776  chfacfpmmul0  22780  ptpjpre2  23498  ptopn2  23502  xkopt  23573  tsmssplit  24070  xrsxmet  24728  htpycc  24909  pco1  24945  pcohtpylem  24949  pcoass  24954  pcorevlem  24956  ovolunlem1a  25427  ovolunlem1  25428  ovolicc1  25447  itg11  25622  mbfi1flim  25654  itg2split  25680  itg2cnlem1  25692  itgeq2  25709  iblss  25736  itgss2  25744  itgss3  25746  itgless  25748  ibladdlem  25751  itgaddlem1  25754  itggt0  25775  itgcn  25776  dvexp2  25888  lhop2  25950  deg1add  26038  ig1pval3  26113  ply1termlem  26138  plyeq0lem  26145  plypf1  26147  dvply1  26221  pserdvlem2  26368  abelthlem9  26380  logtayllem  26598  logtayl  26599  cxpef  26604  rlimcnp2  26906  efrlim  26909  efrlimOLD  26910  muinv  27133  bposlem5  27229  lgsval2lem  27248  lgsval4  27258  lgsval4a  27260  lgsneg  27262  lgsneg1  27263  lgsdilem  27265  lgsdir  27273  lgsne0  27276  gausslemma2dlem1a  27306  gausslemma2dlem3  27309  2lgslem3  27345  2sqnn0  27379  rplogsumlem2  27426  dchrisum0fno1  27452  rplogsum  27468  pntrlog2bndlem4  27521  pntrlog2bndlem5  27522  padicabv  27571  ostth1  27574  ostth3  27579  expsnnval  28352  axlowdim  28943  vtxval  28982  iedgval  28983  funvtxdmge2val  28993  funiedgdmge2val  28994  funvtxdm2val  28995  funiedgdm2val  28996  snstrvtxval  29019  snstriedgval  29020  crctcshwlkn0lem3  29794  crctcsh  29806  clwlkclwwlklem2fv2  29980  eucrct2eupth  30229  fmptunsnop  32687  ind0  32846  ccatws1f1o  32941  pmtridfv1  33073  pmtridfv2  33074  psgnfzto1stlem  33078  elrgspnlem2  33219  elrgspnlem3  33220  elrgspnlem4  33221  elrspunsn  33403  gsummoncoe1fzo  33567  mplmulmvr  33592  esplyfval3  33614  esplyind  33615  extdgfialglem2  33729  rtelextdg2lem  33762  2sqr3minply  33816  cos9thpiminply  33824  smattr  33835  smatbl  33836  smatbr  33837  1smat1  33840  submatminr1  33846  madjusmdetlem1  33863  madjusmdetlem2  33864  xrge0iifcv  33970  xrge0iif1  33974  esumpinfval  34109  sigaclfu2  34157  eulerpartlemgs2  34416  ballotlemrv2  34558  signswmnd  34593  signswlid  34595  signsvtp  34619  signlem0  34623  ex-sategoelelomsuc  35493  ex-sategoelel12  35494  mrsubcn  35586  bcneg1  35803  bccolsum  35806  dfrdg2  35860  dfrdg4  36018  unblimceq0lem  36573  unbdqndv2lem2  36577  finxpreclem3  37460  finxpreclem5  37462  poimirlem1  37684  poimirlem2  37685  poimirlem7  37690  poimirlem10  37693  poimirlem11  37694  poimirlem16  37699  poimirlem17  37700  poimirlem20  37703  poimirlem24  37707  mblfinlem2  37721  itg2addnclem2  37735  ibladdnclem  37739  ftc1anclem6  37761  ftc1anclem8  37763  fdc  37808  heiborlem6  37879  cdleme31fv2  40515  cdlemefr27cl  40525  sticksstones10  42271  sticksstones12a  42273  sticksstones12  42274  evlsbagval  42687  selvvvval  42706  fsuppssind  42714  mhpind  42715  prjspner1  42747  kelac1  43183  flcidc  43290  oe0suclim  43397  oe0rif  43405  cantnfub  43441  cantnfresb  43444  tfsconcatfv  43461  sqrtcval  43761  relexp01min  43833  relexpxpmin  43837  clsk1indlem0  44161  refsum2cnlem1  45161  upbdrech2  45436  ssfiunibd  45437  ioondisj2  45620  limsup10exlem  45897  icccncfext  46012  cncfiooicclem1  46018  cncfioobdlem  46021  dvnxpaek  46067  dvnprodlem1  46071  ditgeqiooicc  46085  iblcncfioo  46103  volioore  46115  dirkercncflem2  46229  dirkercncflem4  46231  fourierdlem40  46272  fourierdlem56  46287  fourierdlem65  46296  fourierdlem66  46297  fourierdlem73  46304  fourierdlem74  46305  fourierdlem75  46306  fourierdlem78  46309  fourierdlem79  46310  fourierdlem81  46312  fourierdlem82  46313  fourierdlem97  46328  fourierdlem103  46334  fourierdlem104  46335  sqwvfoura  46353  sqwvfourb  46354  fourierswlem  46355  fouriersw  46356  etransclem4  46363  etransclem14  46373  etransclem20  46379  etransclem22  46381  etransclem24  46383  etransclem25  46384  etransclem31  46390  etransclem32  46391  etransclem35  46394  sge0reval  46497  sge0sn  46504  nnfoctbdjlem  46580  isomenndlem  46655  ovnn0val  46676  ovnsubaddlem1  46695  hoidmvn0val  46709  hsphoidmvle2  46710  hsphoidmvle  46711  hoidmvval0  46712  hoidmv1lelem2  46717  hoidmvlelem2  46721  hoidmvlelem3  46722  ovnhoilem1  46726  hspmbllem1  46751  hspmbllem2  46752  volico2  46766  ovolval2lem  46768  ovnsubadd2lem  46770  ovolval4lem1  46774  ovnovollem3  46783  vonioo  46807  vonicc  46810  prproropf1olem3  47632  fdmdifeqresdif  48469  dig1  48736  dignn0flhalflem1  48743  itcoval1  48791  itcoval2  48792  itcoval3  48793  itcovalsuc  48795  ackvalsuc1mpt  48806