Theorem iffalsed 4493

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4483

This theorem is used by:  ifeqor  4534  ifnot  4535  ifan  4536  somincom  6128  partfun  6679  mpodifsnif  7528  tz7.44-2  8396  tz7.44-3  8397  unxpdomlem2  9227  sniffsupp  9370  unwdomg  9556  cantnfp1lem1  9657  cantnfp1lem3  9659  cantnflem1d  9667  ttrcltr  9695  updjudhcoinrg  9938  ttukeylem7  10517  canthp1lem2  10662  pwfseqlem3  10669  ind0  12252  xmulneg1  13321  rexmul  13323  xmulpnf1  13326  fzprval  13640  expnnval  14128  expneg  14133  tpf1ofv1  14562  tpf1ofv2  14563  ccatval2  14643  ccatalpha  14660  swrdnd  14724  swrdnd2  14725  swrd0  14728  swrdccatin2  14798  relexpsucnnr  15098  relexp1g  15099  sgnp  15163  sgnn  15167  absmax  15417  sumss2  15812  fsumsplit  15827  fprodntriv  16029  fprodsplit  16053  ef0lem  16164  rpnnen2lem9  16310  sadadd2lem2  16540  sadadd2  16550  eucalgf  16673  eucalginv  16674  eucalglt  16675  iserodd  16927  pcmpt  16984  pcmpt2  16985  ramtub  17104  prmo1  17129  fvprif  17647  gsumval2a  18787  mgm2nsgrplem2  19031  mgm2nsgrplem3  19032  sgrp2nmndlem3  19037  mulgnn  19198  mulgnegnn  19207  symgextfv  19545  pmtrprfv3  19581  pmtrdifellem4  19606  pmtrprfval  19614  pmtrprfvalrn  19615  odlem2  19666  dfod2  19691  gsumval3a  20030  gsumzsplit  20054  dmdprdsplitlem  20166  ablsimpgfind  20239  abvtrivd  20998  uvcvv0  22003  uvcff  22004  psrlidm  22176  psrridm  22177  mvrcl  22206  mplmon  22251  mplmonmul  22252  mplcoe1  22253  mplcoe5  22256  evlslem3  22296  selvvvval  22358  coe1tmfv2  22501  cply1coe0  22526  cply1coe0bi  22527  gsummoncoe1  22533  mulmarep1gsum1  22795  1marepvsma1  22805  mdetunilem2  22835  mdetunilem9  22842  maducoeval2  22862  symgmatr01lem  22875  gsummatr01lem3  22879  gsummatr01lem4  22880  gsummatr01  22881  m2cpm  22966  m2cpminvid2lem  22979  pmatcollpw3fi1lem1  23011  mp2pm2mplem4  23034  chfacffsupp  23081  chfacfscmul0  23083  chfacfpmmul0  23087  ptpjpre2  23806  ptopn2  23810  xkopt  23881  tsmssplit  24378  xrsxmet  25036  htpycc  25208  pco1  25243  pcohtpylem  25247  pcoass  25252  pcorevlem  25254  ovolunlem1a  25724  ovolunlem1  25725  ovolicc1  25744  itg11  25919  mbfi1flim  25951  itg2split  25977  itg2cnlem1  25989  itgeq2  26005  iblss  26032  itgss2  26040  itgss3  26042  itgless  26044  ibladdlem  26047  itgaddlem1  26050  itggt0  26071  itgcn  26072  dvexp2  26181  lhop2  26242  deg1add  26328  ig1pval3  26403  ply1termlem  26428  plyeq0lem  26436  plypf1  26438  dvply1  26514  pserdvlem2  26664  abelthlem9  26676  logtayllem  26896  logtayl  26897  cxpef  26902  rlimcnp2  27203  efrlim  27206  muinv  27429  bposlem5  27524  lgsval2lem  27543  lgsval4  27553  lgsval4a  27555  lgsneg  27557  lgsneg1  27558  lgsdilem  27560  lgsdir  27568  lgsne0  27571  gausslemma2dlem1a  27601  gausslemma2dlem3  27604  2lgslem3  27640  2sqnn0  27674  rplogsumlem2  27721  dchrisum0fno1  27747  rplogsum  27763  pntrlog2bndlem4  27816  pntrlog2bndlem5  27817  padicabv  27866  ostth1  27869  ostth3  27874  expnnsval  28691  angmgmaddov1  29267  axlowdim  29418  vtxval  29457  iedgval  29458  funvtxdmge2val  29468  funiedgdmge2val  29469  funvtxdm2val  29470  funiedgdm2val  29471  snstrvtxval  29494  snstriedgval  29495  crctcshwlkn0lem3  30280  crctcsh  30292  clwlkclwwlklem2fv2  30466  eucrct2eupth  30725  fmptunsnop  33172  ccatws1f1o  33393  pmtridfv1  33535  pmtridfv2  33536  psgnfzto1stlem  33540  elrgspnlem2  33683  elrgspnlem3  33684  elrgspnlem4  33685  elrspunsn  33857  gsummoncoe1fzo  34007  mplasclco  34026  mplmulmvr  34049  evlextv  34052  psrmonmul  34060  esplyfval3  34082  esplyfval1  34083  esplyind  34085  extdgfialglem2  34203  rtelextdg2lem  34236  2sqr3minply  34290  cos9thpiminply  34298  smattr  34309  smatbl  34310  smatbr  34311  1smat1  34314  submatminr1  34320  madjusmdetlem1  34337  madjusmdetlem2  34338  xrge0iifcv  34444  xrge0iif1  34448  esumpinfval  34583  sigaclfu2  34631  eulerpartlemgs2  34891  ballotlemrv2  35033  signswmnd  35065  signswlid  35067  signsvtp  35091  signlem0  35095  ex-sategoelelomsuc  36005  ex-sategoelel12  36006  mrsubcn  36098  bcneg1  36315  bccolsum  36318  dfrdg2  36372  dfrdg4  36530  unblimceq0lem  37203  unbdqndv2lem2  37207  finxpreclem3  38147  finxpreclem5  38149  poimirlem1  38370  poimirlem2  38371  poimirlem7  38376  poimirlem10  38379  poimirlem11  38380  poimirlem16  38385  poimirlem17  38386  poimirlem20  38389  poimirlem24  38393  mblfinlem2  38407  itg2addnclem2  38421  ibladdnclem  38425  ftc1anclem6  38447  ftc1anclem8  38449  fdc  38495  heiborlem6  38566  cdleme31fv2  41266  cdlemefr27cl  41276  sticksstones10  43021  sticksstones12a  43023  sticksstones12  43024  evlsbagval  43432  fsuppssind  43439  mhpind  43440  prjspner1  43472  kelac1  43904  flcidc  44011  oe0suclim  44118  oe0rif  44126  cantnfub  44162  cantnfresb  44165  tfsconcatfv  44182  sqrtcval  44481  relexp01min  44553  relexpxpmin  44557  clsk1indlem0  44881  refsum2cnlem1  45871  upbdrech2  46141  ssfiunibd  46142  ioondisj2  46323  limsup10exlem  46600  icccncfext  46715  cncfiooicclem1  46721  cncfioobdlem  46724  dvnxpaek  46770  dvnprodlem1  46774  ditgeqiooicc  46788  iblcncfioo  46806  volioore  46818  dirkercncflem2  46932  dirkercncflem4  46934  fourierdlem40  46975  fourierdlem56  46990  fourierdlem65  46999  fourierdlem66  47000  fourierdlem73  47007  fourierdlem74  47008  fourierdlem75  47009  fourierdlem78  47012  fourierdlem79  47013  fourierdlem81  47015  fourierdlem82  47016  fourierdlem97  47031  fourierdlem103  47037  fourierdlem104  47038  sqwvfoura  47056  sqwvfourb  47057  fourierswlem  47058  fouriersw  47059  etransclem4  47066  etransclem14  47076  etransclem20  47082  etransclem22  47084  etransclem24  47086  etransclem25  47087  etransclem31  47093  etransclem32  47094  etransclem35  47097  sge0reval  47200  sge0sn  47207  nnfoctbdjlem  47283  isomenndlem  47358  ovnn0val  47379  ovnsubaddlem1  47398  hoidmvn0val  47412  hsphoidmvle2  47413  hsphoidmvle  47414  hoidmvval0  47415  hoidmv1lelem2  47420  hoidmvlelem2  47424  hoidmvlelem3  47425  ovnhoilem1  47429  hspmbllem1  47454  hspmbllem2  47455  volico2  47469  ovolval2lem  47471  ovnsubadd2lem  47473  ovolval4lem1  47477  ovnovollem3  47486  vonioo  47510  vonicc  47513  tmachlem-agreeprod  47765  tmachlem-tpopen  47769  prproropf1olem3  48405  fdmdifeqresdif  49272  dig1  49538  dignn0flhalflem1  49545  itcoval1  49593  itcoval2  49594  itcoval3  49595  itcovalsuc  49597  ackvalsuc1mpt  49608  crosspv2d  50794  crosspv3d  50795  veronesev1lem  50806  veronesev2lem  50807  veronesev3lem  50808  veronesev4lem  50809  veronesev5lem  50810  veronesev6lem  50811  veronesevrowd  50812