Theorem iffalsed 4490

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 4488	. 2 ⊢ (¬ 𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐵)

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4480

This theorem is referenced by:  ifeqor  4531  ifnot  4532  ifan  4533  somincom  6091  partfun  6639  mpodifsnif  7473  tz7.44-2  8338  tz7.44-3  8339  unxpdomlem2  9157  sniffsupp  9303  unwdomg  9489  cantnfp1lem1  9587  cantnfp1lem3  9589  cantnflem1d  9597  ttrcltr  9625  updjudhcoinrg  9845  ttukeylem7  10425  canthp1lem2  10564  pwfseqlem3  10571  xmulneg1  13184  rexmul  13186  xmulpnf1  13189  fzprval  13501  expnnval  13987  expneg  13992  tpf1ofv1  14420  tpf1ofv2  14421  ccatval2  14501  ccatalpha  14517  swrdnd  14578  swrdnd2  14579  swrd0  14582  swrdccatin2  14652  relexpsucnnr  14948  relexp1g  14949  sgnp  15013  sgnn  15017  absmax  15253  sumss2  15649  fsumsplit  15664  fprodntriv  15865  fprodsplit  15889  ef0lem  16001  rpnnen2lem9  16147  sadadd2  16387  eucalgf  16510  eucalginv  16511  eucalglt  16512  iserodd  16763  pcmpt  16820  pcmpt2  16821  ramtub  16940  prmo1  16965  fvprif  17482  gsumval2a  18610  mgm2nsgrplem2  18844  mgm2nsgrplem3  18845  sgrp2nmndlem3  18850  mulgnn  19005  mulgnegnn  19014  symgextfv  19347  pmtrprfv3  19383  pmtrdifellem4  19408  pmtrprfval  19416  pmtrprfvalrn  19417  odlem2  19468  dfod2  19493  gsumval3a  19832  gsumzsplit  19856  dmdprdsplitlem  19968  ablsimpgfind  20041  abvtrivd  20765  uvcvv0  21745  uvcff  21746  psrlidm  21917  psrridm  21918  mvrcl  21947  mplmon  21990  mplmonmul  21991  mplcoe1  21992  mplcoe5  21995  evlslem3  22035  coe1tmfv2  22217  cply1coe0  22245  cply1coe0bi  22246  gsummoncoe1  22252  mulmarep1gsum1  22517  1marepvsma1  22527  mdetunilem2  22557  mdetunilem9  22564  maducoeval2  22584  symgmatr01lem  22597  gsummatr01lem3  22601  gsummatr01lem4  22602  gsummatr01  22603  m2cpm  22685  m2cpminvid2lem  22698  pmatcollpw3fi1lem1  22730  mp2pm2mplem4  22753  chfacffsupp  22800  chfacfscmul0  22802  chfacfpmmul0  22806  ptpjpre2  23524  ptopn2  23528  xkopt  23599  tsmssplit  24096  xrsxmet  24754  htpycc  24935  pco1  24971  pcohtpylem  24975  pcoass  24980  pcorevlem  24982  ovolunlem1a  25453  ovolunlem1  25454  ovolicc1  25473  itg11  25648  mbfi1flim  25680  itg2split  25706  itg2cnlem1  25718  itgeq2  25735  iblss  25762  itgss2  25770  itgss3  25772  itgless  25774  ibladdlem  25777  itgaddlem1  25780  itggt0  25801  itgcn  25802  dvexp2  25914  lhop2  25976  deg1add  26064  ig1pval3  26139  ply1termlem  26164  plyeq0lem  26171  plypf1  26173  dvply1  26247  pserdvlem2  26394  abelthlem9  26406  logtayllem  26624  logtayl  26625  cxpef  26630  rlimcnp2  26932  efrlim  26935  efrlimOLD  26936  muinv  27159  bposlem5  27255  lgsval2lem  27274  lgsval4  27284  lgsval4a  27286  lgsneg  27288  lgsneg1  27289  lgsdilem  27291  lgsdir  27299  lgsne0  27302  gausslemma2dlem1a  27332  gausslemma2dlem3  27335  2lgslem3  27371  2sqnn0  27405  rplogsumlem2  27452  dchrisum0fno1  27478  rplogsum  27494  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  padicabv  27597  ostth1  27600  ostth3  27605  expnnsval  28422  axlowdim  29034  vtxval  29073  iedgval  29074  funvtxdmge2val  29084  funiedgdmge2val  29085  funvtxdm2val  29086  funiedgdm2val  29087  snstrvtxval  29110  snstriedgval  29111  crctcshwlkn0lem3  29885  crctcsh  29897  clwlkclwwlklem2fv2  30071  eucrct2eupth  30320  fmptunsnop  32779  ind0  32937  ccatws1f1o  33033  pmtridfv1  33177  pmtridfv2  33178  psgnfzto1stlem  33182  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnlem4  33327  elrspunsn  33510  gsummoncoe1fzo  33678  mplmulmvr  33704  evlextv  33707  esplyfval3  33730  esplyind  33731  extdgfialglem2  33850  rtelextdg2lem  33883  2sqr3minply  33937  cos9thpiminply  33945  smattr  33956  smatbl  33957  smatbr  33958  1smat1  33961  submatminr1  33967  madjusmdetlem1  33984  madjusmdetlem2  33985  xrge0iifcv  34091  xrge0iif1  34095  esumpinfval  34230  sigaclfu2  34278  eulerpartlemgs2  34537  ballotlemrv2  34679  signswmnd  34714  signswlid  34716  signsvtp  34740  signlem0  34744  ex-sategoelelomsuc  35620  ex-sategoelel12  35621  mrsubcn  35713  bcneg1  35930  bccolsum  35933  dfrdg2  35987  dfrdg4  36145  unblimceq0lem  36706  unbdqndv2lem2  36710  finxpreclem3  37598  finxpreclem5  37600  poimirlem1  37822  poimirlem2  37823  poimirlem7  37828  poimirlem10  37831  poimirlem11  37832  poimirlem16  37837  poimirlem17  37838  poimirlem20  37841  poimirlem24  37845  mblfinlem2  37859  itg2addnclem2  37873  ibladdnclem  37877  ftc1anclem6  37899  ftc1anclem8  37901  fdc  37946  heiborlem6  38017  cdleme31fv2  40653  cdlemefr27cl  40663  sticksstones10  42409  sticksstones12a  42411  sticksstones12  42412  evlsbagval  42812  selvvvval  42828  fsuppssind  42836  mhpind  42837  prjspner1  42869  kelac1  43305  flcidc  43412  oe0suclim  43519  oe0rif  43527  cantnfub  43563  cantnfresb  43566  tfsconcatfv  43583  sqrtcval  43882  relexp01min  43954  relexpxpmin  43958  clsk1indlem0  44282  refsum2cnlem1  45282  upbdrech2  45556  ssfiunibd  45557  ioondisj2  45739  limsup10exlem  46016  icccncfext  46131  cncfiooicclem1  46137  cncfioobdlem  46140  dvnxpaek  46186  dvnprodlem1  46190  ditgeqiooicc  46204  iblcncfioo  46222  volioore  46234  dirkercncflem2  46348  dirkercncflem4  46350  fourierdlem40  46391  fourierdlem56  46406  fourierdlem65  46415  fourierdlem66  46416  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem78  46428  fourierdlem79  46429  fourierdlem81  46431  fourierdlem82  46432  fourierdlem97  46447  fourierdlem103  46453  fourierdlem104  46454  sqwvfoura  46472  sqwvfourb  46473  fourierswlem  46474  fouriersw  46475  etransclem4  46482  etransclem14  46492  etransclem20  46498  etransclem22  46500  etransclem24  46502  etransclem25  46503  etransclem31  46509  etransclem32  46510  etransclem35  46513  sge0reval  46616  sge0sn  46623  nnfoctbdjlem  46699  isomenndlem  46774  ovnn0val  46795  ovnsubaddlem1  46814  hoidmvn0val  46828  hsphoidmvle2  46829  hsphoidmvle  46830  hoidmvval0  46831  hoidmv1lelem2  46836  hoidmvlelem2  46840  hoidmvlelem3  46841  ovnhoilem1  46845  hspmbllem1  46870  hspmbllem2  46871  volico2  46885  ovolval2lem  46887  ovnsubadd2lem  46889  ovolval4lem1  46893  ovnovollem3  46902  vonioo  46926  vonicc  46929  prproropf1olem3  47751  fdmdifeqresdif  48588  dig1  48854  dignn0flhalflem1  48861  itcoval1  48909  itcoval2  48910  itcoval3  48911  itcovalsuc  48913  ackvalsuc1mpt  48924