Theorem iffalsed 4496

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-if 4486

This theorem is used by:  ifeqor  4537  ifnot  4538  ifan  4539  somincom  6144  partfun  6714  mpodifsnif  7564  tz7.44-2  8451  tz7.44-3  8452  unxpdomlem2  9284  sniffsupp  9427  unwdomg  9613  cantnfp1lem1  9714  cantnfp1lem3  9716  cantnflem1d  9724  ttrcltr  9752  updjudhcoinrg  10049  ttukeylem7  10630  canthp1lem2  10775  pwfseqlem3  10782  ind0  12368  xmulneg1  13437  rexmul  13439  xmulpnf1  13442  fzprval  13757  expnnval  14245  expneg  14250  tpf1ofv1  14681  tpf1ofv2  14682  ccatval2  14762  ccatalpha  14779  swrdnd  14844  swrdnd2  14845  swrd0  14848  swrdccatin2  14918  relexpsucnnr  15219  relexp1g  15220  sgnp  15284  sgnn  15288  absmax  15538  sumss2  15933  fsumsplit  15948  fprodntriv  16150  fprodsplit  16174  ef0lem  16285  rpnnen2lem9  16431  sadadd2lem2  16661  sadadd2  16671  eucalgf  16799  eucalginv  16800  eucalglt  16801  iserodd  17054  pcmpt  17111  pcmpt2  17112  ramtub  17231  prmo1  17256  fvprif  17774  gsumval2a  18915  mgm2nsgrplem2  19159  mgm2nsgrplem3  19160  sgrp2nmndlem3  19165  mulgnn  19326  mulgnegnn  19335  symgextfv  19674  pmtrprfv3  19710  pmtrdifellem4  19735  pmtrprfval  19743  pmtrprfvalrn  19744  odlem2  19795  dfod2  19820  gsumval3a  20159  gsumzsplit  20183  dmdprdsplitlem  20295  ablsimpgfind  20368  abvtrivd  21131  uvcvv0  22140  uvcff  22141  psrlidm  22313  psrridm  22314  mvrcl  22343  mplmon  22388  mplmonmul  22389  mplcoe1  22390  mplcoe5  22393  evlslem3  22433  selvvvval  22495  coe1tmfv2  22638  cply1coe0  22663  cply1coe0bi  22664  gsummoncoe1  22670  mulmarep1gsum1  22932  1marepvsma1  22942  mdetunilem2  22972  mdetunilem9  22979  maducoeval2  22999  symgmatr01lem  23012  gsummatr01lem3  23016  gsummatr01lem4  23017  gsummatr01  23018  m2cpm  23103  m2cpminvid2lem  23116  pmatcollpw3fi1lem1  23148  mp2pm2mplem4  23171  chfacffsupp  23218  chfacfscmul0  23220  chfacfpmmul0  23224  ptpjpre2  23943  ptopn2  23947  xkopt  24018  tsmssplit  24515  xrsxmet  25173  htpycc  25345  pco1  25380  pcohtpylem  25384  pcoass  25389  pcorevlem  25391  ovolunlem1a  25861  ovolunlem1  25862  ovolicc1  25881  itg11  26056  mbfi1flim  26088  itg2split  26114  itg2cnlem1  26126  itgeq2  26142  iblss  26169  itgss2  26177  itgss3  26179  itgless  26181  ibladdlem  26184  itgaddlem1  26187  itggt0  26208  itgcn  26209  dvexp2  26318  lhop2  26379  deg1add  26465  ig1pval3  26540  ply1termlem  26565  plyeq0lem  26573  plypf1  26575  dvply1  26649  pserdvlem2  26801  abelthlem9  26813  logtayllem  27033  logtayl  27034  cxpef  27039  rlimcnp2  27340  efrlim  27343  muinv  27566  bposlem5  27661  lgsval2lem  27680  lgsval4  27690  lgsval4a  27692  lgsneg  27694  lgsneg1  27695  lgsdilem  27697  lgsdir  27705  lgsne0  27708  gausslemma2dlem1a  27738  gausslemma2dlem3  27741  2lgslem3  27777  2sqnn0  27811  rplogsumlem2  27858  dchrisum0fno1  27884  rplogsum  27900  pntrlog2bndlem4  27953  pntrlog2bndlem5  27954  padicabv  28003  ostth1  28006  ostth3  28011  expnnsval  28858  angmgmaddov1  29434  axlowdim  29585  vtxval  29624  iedgval  29625  funvtxdmge2val  29635  funiedgdmge2val  29636  funvtxdm2val  29637  funiedgdm2val  29638  snstrvtxval  29661  snstriedgval  29662  crctcshwlkn0lem3  30447  crctcsh  30459  clwlkclwwlklem2fv2  30633  eucrct2eupth  30892  fmptunsnop  33380  ccatws1f1o  33600  pmtridfv1  33745  pmtridfv2  33746  psgnfzto1stlem  33750  elrgspnlem2  33893  elrgspnlem3  33894  elrgspnlem4  33895  elrspunsn  34076  gsummoncoe1fzo  34225  rngunsnply1chr2lem2  34244  mplasclco  34252  mplmulmvr  34275  evlextv  34278  psrmonmul  34286  esplyfval3  34308  esplyfval1  34309  esplyind  34311  extdgfialglem2  34429  rtelextdg2lem  34462  2sqr3minply  34516  cos9thpiminply  34524  smattr  34535  smatbl  34536  smatbr  34537  1smat1  34540  submatminr1  34546  madjusmdetlem1  34563  madjusmdetlem2  34564  xrge0iifcv  34670  xrge0iif1  34674  esumpinfval  34809  sigaclfu2  34857  eulerpartlemgs2  35116  ballotlemrv2  35258  signswmnd  35290  signswlid  35292  signsvtp  35316  signlem0  35320  gdlopcfvlem  36005  fnlfvk3n0  36062  ex-sategoelelomsuc  36392  ex-sategoelel12  36393  mrsubcn  36485  bcneg1  36709  bccolsum  36712  dfrdg2  36765  dfrdg4  36923  unblimceq0lem  37580  unbdqndv2lem2  37584  finxpreclem3  38577  finxpreclem5  38579  poimirlem1  38800  poimirlem2  38801  poimirlem7  38806  poimirlem10  38809  poimirlem11  38810  poimirlem16  38815  poimirlem17  38816  poimirlem20  38819  poimirlem24  38823  mblfinlem2  38837  itg2addnclem2  38851  ibladdnclem  38855  ftc1anclem6  38877  ftc1anclem8  38879  fdc  38938  heiborlem6  39009  cdleme31fv2  41709  cdlemefr27cl  41719  sticksstones10  43464  sticksstones12a  43466  sticksstones12  43467  evlsbagval  43874  fsuppssind  43881  mhpind  43882  kelac1  44325  flcidc  44427  oe0suclim  44534  oe0rif  44542  cantnfub  44578  cantnfresb  44581  tfsconcatfv  44598  sqrtcval  44896  relexp01min  44968  relexpxpmin  44972  clsk1indlem0  45296  refsum2cnlem1  46322  upbdrech2  46591  ssfiunibd  46592  ioondisj2  46772  limsup10exlem  47049  icccncfext  47164  cncfiooicclem1  47170  cncfioobdlem  47173  dvnxpaek  47219  dvnprodlem1  47223  ditgeqiooicc  47237  iblcncfioo  47255  volioore  47267  dirkercncflem2  47381  dirkercncflem4  47383  fourierdlem40  47424  fourierdlem56  47439  fourierdlem65  47448  fourierdlem66  47449  fourierdlem73  47456  fourierdlem74  47457  fourierdlem75  47458  fourierdlem78  47461  fourierdlem79  47462  fourierdlem81  47464  fourierdlem82  47465  fourierdlem97  47480  fourierdlem103  47486  fourierdlem104  47487  sqwvfoura  47505  sqwvfourb  47506  fourierswlem  47507  fouriersw  47508  etransclem4  47515  etransclem14  47525  etransclem20  47531  etransclem22  47533  etransclem24  47535  etransclem25  47536  etransclem31  47542  etransclem32  47543  etransclem35  47546  sge0reval  47649  sge0sn  47656  nnfoctbdjlem  47732  isomenndlem  47807  ovnn0val  47828  ovnsubaddlem1  47847  hoidmvn0val  47861  hsphoidmvle2  47862  hsphoidmvle  47863  hoidmvval0  47864  hoidmv1lelem2  47869  hoidmvlelem2  47873  hoidmvlelem3  47874  ovnhoilem1  47878  hspmbllem1  47903  hspmbllem2  47904  volico2  47918  ovolval2lem  47920  ovnsubadd2lem  47922  ovolval4lem1  47926  ovnovollem3  47935  vonioo  47959  vonicc  47962  tmachlem-agreeprod  48214  tmachlem-tpopen  48218  prproropf1olem3  48854  linply2cfv  49706  fdmdifeqresdif  49779  dig1  50045  dignn0flhalflem1  50052  itcoval1  50100  itcoval2  50101  itcoval3  50102  itcovalsuc  50104  ackvalsuc1mpt  50115  parhomne  51080  parcoval2  51091  parmapcl  51096  parswapprop  51102  crosspv2d  51383  crosspv3d  51384  veronesev1lem  51395  veronesev2lem  51396  veronesev3lem  51397  veronesev4lem  51398  veronesev5lem  51399  veronesev6lem  51400  veronesevrowd  51401