Theorem iffalsed 4494

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1563  ifcif 4483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4484

This theorem is referenced by:  ifeqor  4535  ifnot  4536  ifan  4537  somincom  6124  partfun  6672  mpodifsnif  7515  tz7.44-2  8382  tz7.44-3  8383  unxpdomlem2  9205  sniffsupp  9348  unwdomg  9534  cantnfp1lem1  9635  cantnfp1lem3  9637  cantnflem1d  9645  ttrcltr  9673  updjudhcoinrg  9907  ttukeylem7  10487  canthp1lem2  10626  pwfseqlem3  10633  ind0  12216  xmulneg1  13283  rexmul  13285  xmulpnf1  13288  fzprval  13601  expnnval  14088  expneg  14093  tpf1ofv1  14522  tpf1ofv2  14523  ccatval2  14603  ccatalpha  14619  swrdnd  14680  swrdnd2  14681  swrd0  14684  swrdccatin2  14754  relexpsucnnr  15050  relexp1g  15051  sgnp  15115  sgnn  15119  absmax  15369  sumss2  15765  fsumsplit  15780  fprodntriv  15984  fprodsplit  16008  ef0lem  16120  rpnnen2lem9  16266  sadadd2  16506  eucalgf  16629  eucalginv  16630  eucalglt  16631  iserodd  16883  pcmpt  16940  pcmpt2  16941  ramtub  17060  prmo1  17085  fvprif  17603  gsumval2a  18731  mgm2nsgrplem2  18969  mgm2nsgrplem3  18970  sgrp2nmndlem3  18975  mulgnn  19129  mulgnegnn  19138  symgextfv  19476  pmtrprfv3  19512  pmtrdifellem4  19537  pmtrprfval  19545  pmtrprfvalrn  19546  odlem2  19597  dfod2  19622  gsumval3a  19961  gsumzsplit  19985  dmdprdsplitlem  20097  ablsimpgfind  20170  abvtrivd  20901  uvcvv0  21897  uvcff  21898  psrlidm  22068  psrridm  22069  mvrcl  22098  mplmon  22143  mplmonmul  22144  mplcoe1  22145  mplcoe5  22148  evlslem3  22188  selvvvval  22250  coe1tmfv2  22393  cply1coe0  22418  cply1coe0bi  22419  gsummoncoe1  22425  mulmarep1gsum1  22687  1marepvsma1  22697  mdetunilem2  22727  mdetunilem9  22734  maducoeval2  22754  symgmatr01lem  22767  gsummatr01lem3  22771  gsummatr01lem4  22772  gsummatr01  22773  m2cpm  22855  m2cpminvid2lem  22868  pmatcollpw3fi1lem1  22900  mp2pm2mplem4  22923  chfacffsupp  22970  chfacfscmul0  22972  chfacfpmmul0  22976  ptpjpre2  23694  ptopn2  23698  xkopt  23769  tsmssplit  24266  xrsxmet  24924  htpycc  25096  pco1  25131  pcohtpylem  25135  pcoass  25140  pcorevlem  25142  ovolunlem1a  25612  ovolunlem1  25613  ovolicc1  25632  itg11  25807  mbfi1flim  25839  itg2split  25865  itg2cnlem1  25877  itgeq2  25894  iblss  25921  itgss2  25929  itgss3  25931  itgless  25933  ibladdlem  25936  itgaddlem1  25939  itggt0  25960  itgcn  25961  dvexp2  26070  lhop2  26131  deg1add  26217  ig1pval3  26292  ply1termlem  26317  plyeq0lem  26324  plypf1  26326  dvply1  26402  pserdvlem2  26545  abelthlem9  26557  logtayllem  26778  logtayl  26779  cxpef  26784  rlimcnp2  27085  efrlim  27088  muinv  27311  bposlem5  27406  lgsval2lem  27425  lgsval4  27435  lgsval4a  27437  lgsneg  27439  lgsneg1  27440  lgsdilem  27442  lgsdir  27450  lgsne0  27453  gausslemma2dlem1a  27483  gausslemma2dlem3  27486  2lgslem3  27522  2sqnn0  27556  rplogsumlem2  27603  dchrisum0fno1  27629  rplogsum  27645  pntrlog2bndlem4  27698  pntrlog2bndlem5  27699  padicabv  27748  ostth1  27751  ostth3  27756  expnnsval  28573  axlowdim  29216  vtxval  29255  iedgval  29256  funvtxdmge2val  29266  funiedgdmge2val  29267  funvtxdm2val  29268  funiedgdm2val  29269  snstrvtxval  29292  snstriedgval  29293  crctcshwlkn0lem3  30066  crctcsh  30078  clwlkclwwlklem2fv2  30252  eucrct2eupth  30501  fmptunsnop  32953  ccatws1f1o  33179  pmtridfv1  33323  pmtridfv2  33324  psgnfzto1stlem  33328  elrgspnlem2  33471  elrgspnlem3  33472  elrgspnlem4  33473  elrspunsn  33648  gsummoncoe1fzo  33799  mplasclco  33818  mplmulmvr  33841  evlextv  33844  psrmonmul  33852  esplyfval3  33874  esplyfval1  33875  esplyind  33877  extdgfialglem2  33995  rtelextdg2lem  34028  2sqr3minply  34082  cos9thpiminply  34090  smattr  34101  smatbl  34102  smatbr  34103  1smat1  34106  submatminr1  34112  madjusmdetlem1  34129  madjusmdetlem2  34130  xrge0iifcv  34236  xrge0iif1  34240  esumpinfval  34375  sigaclfu2  34423  eulerpartlemgs2  34682  ballotlemrv2  34824  signswmnd  34856  signswlid  34858  signsvtp  34882  signlem0  34886  ex-sategoelelomsuc  35784  ex-sategoelel12  35785  mrsubcn  35877  bcneg1  36094  bccolsum  36097  dfrdg2  36151  dfrdg4  36309  unblimceq0lem  36952  unbdqndv2lem2  36956  finxpreclem3  37894  finxpreclem5  37896  poimirlem1  38127  poimirlem2  38128  poimirlem7  38133  poimirlem10  38136  poimirlem11  38137  poimirlem16  38142  poimirlem17  38143  poimirlem20  38146  poimirlem24  38150  mblfinlem2  38164  itg2addnclem2  38178  ibladdnclem  38182  ftc1anclem6  38204  ftc1anclem8  38206  fdc  38251  heiborlem6  38322  cdleme31fv2  41024  cdlemefr27cl  41034  sticksstones10  42779  sticksstones12a  42781  sticksstones12  42782  evlsbagval  43175  fsuppssind  43182  mhpind  43183  prjspner1  43215  kelac1  43647  flcidc  43754  oe0suclim  43861  oe0rif  43869  cantnfub  43905  cantnfresb  43908  tfsconcatfv  43925  sqrtcval  44224  relexp01min  44296  relexpxpmin  44300  clsk1indlem0  44624  refsum2cnlem1  45616  upbdrech2  45886  ssfiunibd  45887  ioondisj2  46068  limsup10exlem  46345  icccncfext  46460  cncfiooicclem1  46466  cncfioobdlem  46469  dvnxpaek  46515  dvnprodlem1  46519  ditgeqiooicc  46533  iblcncfioo  46551  volioore  46563  dirkercncflem2  46677  dirkercncflem4  46679  fourierdlem40  46720  fourierdlem56  46735  fourierdlem65  46744  fourierdlem66  46745  fourierdlem73  46752  fourierdlem74  46753  fourierdlem75  46754  fourierdlem78  46757  fourierdlem79  46758  fourierdlem81  46760  fourierdlem82  46761  fourierdlem97  46776  fourierdlem103  46782  fourierdlem104  46783  sqwvfoura  46801  sqwvfourb  46802  fourierswlem  46803  fouriersw  46804  etransclem4  46811  etransclem14  46821  etransclem20  46827  etransclem22  46829  etransclem24  46831  etransclem25  46832  etransclem31  46838  etransclem32  46839  etransclem35  46842  sge0reval  46945  sge0sn  46952  nnfoctbdjlem  47028  isomenndlem  47103  ovnn0val  47124  ovnsubaddlem1  47143  hoidmvn0val  47157  hsphoidmvle2  47158  hsphoidmvle  47159  hoidmvval0  47160  hoidmv1lelem2  47165  hoidmvlelem2  47169  hoidmvlelem3  47170  ovnhoilem1  47174  hspmbllem1  47199  hspmbllem2  47200  volico2  47214  ovolval2lem  47216  ovnsubadd2lem  47218  ovolval4lem1  47222  ovnovollem3  47231  vonioo  47255  vonicc  47258  prproropf1olem3  48110  fdmdifeqresdif  48974  dig1  49240  dignn0flhalflem1  49247  itcoval1  49295  itcoval2  49296  itcoval3  49297  itcovalsuc  49299  ackvalsuc1mpt  49310