Theorem iffalsed 4492

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  ifeqor  4533  ifnot  4534  ifan  4535  somincom  6127  partfun  6687  mpodifsnif  7536  tz7.44-2  8419  tz7.44-3  8420  unxpdomlem2  9252  sniffsupp  9396  unwdomg  9582  cantnfp1lem1  9683  cantnfp1lem3  9685  cantnflem1d  9693  ttrcltr  9721  updjudhcoinrg  10018  ttukeylem7  10597  canthp1lem2  10742  pwfseqlem3  10749  ind0  12334  xmulneg1  13403  rexmul  13405  xmulpnf1  13408  fzprval  13723  expnnval  14211  expneg  14216  tpf1ofv1  14646  tpf1ofv2  14647  ccatval2  14727  ccatalpha  14744  swrdnd  14809  swrdnd2  14810  swrd0  14813  swrdccatin2  14883  relexpsucnnr  15184  relexp1g  15185  sgnp  15249  sgnn  15253  absmax  15503  sumss2  15898  fsumsplit  15913  fprodntriv  16115  fprodsplit  16139  ef0lem  16250  rpnnen2lem9  16396  sadadd2lem2  16626  sadadd2  16636  eucalgf  16764  eucalginv  16765  eucalglt  16766  iserodd  17019  pcmpt  17076  pcmpt2  17077  ramtub  17196  prmo1  17221  fvprif  17739  gsumval2a  18880  mgm2nsgrplem2  19124  mgm2nsgrplem3  19125  sgrp2nmndlem3  19130  mulgnn  19291  mulgnegnn  19300  symgextfv  19638  pmtrprfv3  19674  pmtrdifellem4  19699  pmtrprfval  19707  pmtrprfvalrn  19708  odlem2  19759  dfod2  19784  gsumval3a  20123  gsumzsplit  20147  dmdprdsplitlem  20259  ablsimpgfind  20332  abvtrivd  21095  uvcvv0  22102  uvcff  22103  psrlidm  22275  psrridm  22276  mvrcl  22305  mplmon  22350  mplmonmul  22351  mplcoe1  22352  mplcoe5  22355  evlslem3  22395  selvvvval  22457  coe1tmfv2  22600  cply1coe0  22625  cply1coe0bi  22626  gsummoncoe1  22632  mulmarep1gsum1  22894  1marepvsma1  22904  mdetunilem2  22934  mdetunilem9  22941  maducoeval2  22961  symgmatr01lem  22974  gsummatr01lem3  22978  gsummatr01lem4  22979  gsummatr01  22980  m2cpm  23065  m2cpminvid2lem  23078  pmatcollpw3fi1lem1  23110  mp2pm2mplem4  23133  chfacffsupp  23180  chfacfscmul0  23182  chfacfpmmul0  23186  ptpjpre2  23905  ptopn2  23909  xkopt  23980  tsmssplit  24477  xrsxmet  25135  htpycc  25307  pco1  25342  pcohtpylem  25346  pcoass  25351  pcorevlem  25353  ovolunlem1a  25823  ovolunlem1  25824  ovolicc1  25843  itg11  26018  mbfi1flim  26050  itg2split  26076  itg2cnlem1  26088  itgeq2  26104  iblss  26131  itgss2  26139  itgss3  26141  itgless  26143  ibladdlem  26146  itgaddlem1  26149  itggt0  26170  itgcn  26171  dvexp2  26280  lhop2  26341  deg1add  26427  ig1pval3  26502  ply1termlem  26527  plyeq0lem  26535  plypf1  26537  dvply1  26611  pserdvlem2  26761  abelthlem9  26773  logtayllem  26993  logtayl  26994  cxpef  26999  rlimcnp2  27300  efrlim  27303  muinv  27526  bposlem5  27621  lgsval2lem  27640  lgsval4  27650  lgsval4a  27652  lgsneg  27654  lgsneg1  27655  lgsdilem  27657  lgsdir  27665  lgsne0  27668  gausslemma2dlem1a  27698  gausslemma2dlem3  27701  2lgslem3  27737  2sqnn0  27771  rplogsumlem2  27818  dchrisum0fno1  27844  rplogsum  27860  pntrlog2bndlem4  27913  pntrlog2bndlem5  27914  padicabv  27963  ostth1  27966  ostth3  27971  expnnsval  28818  angmgmaddov1  29394  axlowdim  29545  vtxval  29584  iedgval  29585  funvtxdmge2val  29595  funiedgdmge2val  29596  funvtxdm2val  29597  funiedgdm2val  29598  snstrvtxval  29621  snstriedgval  29622  crctcshwlkn0lem3  30407  crctcsh  30419  clwlkclwwlklem2fv2  30593  eucrct2eupth  30852  fmptunsnop  33341  ccatws1f1o  33561  pmtridfv1  33703  pmtridfv2  33704  psgnfzto1stlem  33708  elrgspnlem2  33851  elrgspnlem3  33852  elrgspnlem4  33853  elrspunsn  34026  gsummoncoe1fzo  34176  mplasclco  34195  mplmulmvr  34218  evlextv  34221  psrmonmul  34229  esplyfval3  34251  esplyfval1  34252  esplyind  34254  extdgfialglem2  34372  rtelextdg2lem  34405  2sqr3minply  34459  cos9thpiminply  34467  smattr  34478  smatbl  34479  smatbr  34480  1smat1  34483  submatminr1  34489  madjusmdetlem1  34506  madjusmdetlem2  34507  xrge0iifcv  34613  xrge0iif1  34617  esumpinfval  34752  sigaclfu2  34800  eulerpartlemgs2  35059  ballotlemrv2  35201  signswmnd  35233  signswlid  35235  signsvtp  35259  signlem0  35263  ex-sategoelelomsuc  36278  ex-sategoelel12  36279  mrsubcn  36371  bcneg1  36594  bccolsum  36597  dfrdg2  36650  dfrdg4  36808  unblimceq0lem  37465  unbdqndv2lem2  37469  finxpreclem3  38410  finxpreclem5  38412  poimirlem1  38633  poimirlem2  38634  poimirlem7  38639  poimirlem10  38642  poimirlem11  38643  poimirlem16  38648  poimirlem17  38649  poimirlem20  38652  poimirlem24  38656  mblfinlem2  38670  itg2addnclem2  38684  ibladdnclem  38688  ftc1anclem6  38710  ftc1anclem8  38712  fdc  38773  heiborlem6  38844  cdleme31fv2  41544  cdlemefr27cl  41554  sticksstones10  43299  sticksstones12a  43301  sticksstones12  43302  evlsbagval  43708  fsuppssind  43715  mhpind  43716  kelac1  44159  flcidc  44266  oe0suclim  44373  oe0rif  44381  cantnfub  44417  cantnfresb  44420  tfsconcatfv  44437  sqrtcval  44735  relexp01min  44807  relexpxpmin  44811  clsk1indlem0  45135  refsum2cnlem1  46148  upbdrech2  46418  ssfiunibd  46419  ioondisj2  46599  limsup10exlem  46876  icccncfext  46991  cncfiooicclem1  46997  cncfioobdlem  47000  dvnxpaek  47046  dvnprodlem1  47050  ditgeqiooicc  47064  iblcncfioo  47082  volioore  47094  dirkercncflem2  47208  dirkercncflem4  47210  fourierdlem40  47251  fourierdlem56  47266  fourierdlem65  47275  fourierdlem66  47276  fourierdlem73  47283  fourierdlem74  47284  fourierdlem75  47285  fourierdlem78  47288  fourierdlem79  47289  fourierdlem81  47291  fourierdlem82  47292  fourierdlem97  47307  fourierdlem103  47313  fourierdlem104  47314  sqwvfoura  47332  sqwvfourb  47333  fourierswlem  47334  fouriersw  47335  etransclem4  47342  etransclem14  47352  etransclem20  47358  etransclem22  47360  etransclem24  47362  etransclem25  47363  etransclem31  47369  etransclem32  47370  etransclem35  47373  sge0reval  47476  sge0sn  47483  nnfoctbdjlem  47559  isomenndlem  47634  ovnn0val  47655  ovnsubaddlem1  47674  hoidmvn0val  47688  hsphoidmvle2  47689  hsphoidmvle  47690  hoidmvval0  47691  hoidmv1lelem2  47696  hoidmvlelem2  47700  hoidmvlelem3  47701  ovnhoilem1  47705  hspmbllem1  47730  hspmbllem2  47731  volico2  47745  ovolval2lem  47747  ovnsubadd2lem  47749  ovolval4lem1  47753  ovnovollem3  47762  vonioo  47786  vonicc  47789  tmachlem-agreeprod  48041  tmachlem-tpopen  48045  prproropf1olem3  48681  fdmdifeqresdif  49548  dig1  49814  dignn0flhalflem1  49821  itcoval1  49869  itcoval2  49870  itcoval3  49871  itcovalsuc  49873  ackvalsuc1mpt  49884  parhomne  50849  parcoval2  50860  parmapcl  50865  parswapprop  50871  crosspv2d  51130  crosspv3d  51131  veronesev1lem  51142  veronesev2lem  51143  veronesev3lem  51144  veronesev4lem  51145  veronesev5lem  51146  veronesev6lem  51147  veronesevrowd  51148