Theorem iffalsed 4499

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4489

This theorem is referenced by:  ifeqor  4540  ifnot  4541  ifan  4542  somincom  6136  partfun  6684  mpodifsnif  7527  tz7.44-2  8395  tz7.44-3  8396  unxpdomlem2  9218  sniffsupp  9361  unwdomg  9547  cantnfp1lem1  9648  cantnfp1lem3  9650  cantnflem1d  9658  ttrcltr  9686  updjudhcoinrg  9920  ttukeylem7  10500  canthp1lem2  10639  pwfseqlem3  10646  ind0  12229  xmulneg1  13296  rexmul  13298  xmulpnf1  13301  fzprval  13615  expnnval  14102  expneg  14107  tpf1ofv1  14536  tpf1ofv2  14537  ccatval2  14617  ccatalpha  14633  swrdnd  14694  swrdnd2  14695  swrd0  14698  swrdccatin2  14768  relexpsucnnr  15064  relexp1g  15065  sgnp  15129  sgnn  15133  absmax  15383  sumss2  15779  fsumsplit  15794  fprodntriv  15998  fprodsplit  16022  ef0lem  16133  rpnnen2lem9  16279  sadadd2  16519  eucalgf  16642  eucalginv  16643  eucalglt  16644  iserodd  16896  pcmpt  16953  pcmpt2  16954  ramtub  17073  prmo1  17098  fvprif  17616  gsumval2a  18744  mgm2nsgrplem2  18982  mgm2nsgrplem3  18983  sgrp2nmndlem3  18988  mulgnn  19142  mulgnegnn  19151  symgextfv  19489  pmtrprfv3  19525  pmtrdifellem4  19550  pmtrprfval  19558  pmtrprfvalrn  19559  odlem2  19610  dfod2  19635  gsumval3a  19974  gsumzsplit  19998  dmdprdsplitlem  20110  ablsimpgfind  20183  abvtrivd  20916  uvcvv0  21921  uvcff  21922  psrlidm  22092  psrridm  22093  mvrcl  22122  mplmon  22167  mplmonmul  22168  mplcoe1  22169  mplcoe5  22172  evlslem3  22212  selvvvval  22274  coe1tmfv2  22417  cply1coe0  22442  cply1coe0bi  22443  gsummoncoe1  22449  mulmarep1gsum1  22711  1marepvsma1  22721  mdetunilem2  22751  mdetunilem9  22758  maducoeval2  22778  symgmatr01lem  22791  gsummatr01lem3  22795  gsummatr01lem4  22796  gsummatr01  22797  m2cpm  22879  m2cpminvid2lem  22892  pmatcollpw3fi1lem1  22924  mp2pm2mplem4  22947  chfacffsupp  22994  chfacfscmul0  22996  chfacfpmmul0  23000  ptpjpre2  23718  ptopn2  23722  xkopt  23793  tsmssplit  24290  xrsxmet  24948  htpycc  25120  pco1  25155  pcohtpylem  25159  pcoass  25164  pcorevlem  25166  ovolunlem1a  25636  ovolunlem1  25637  ovolicc1  25656  itg11  25831  mbfi1flim  25863  itg2split  25889  itg2cnlem1  25901  itgeq2  25918  iblss  25945  itgss2  25953  itgss3  25955  itgless  25957  ibladdlem  25960  itgaddlem1  25963  itggt0  25984  itgcn  25985  dvexp2  26094  lhop2  26155  deg1add  26241  ig1pval3  26316  ply1termlem  26341  plyeq0lem  26348  plypf1  26350  dvply1  26426  pserdvlem2  26572  abelthlem9  26584  logtayllem  26805  logtayl  26806  cxpef  26811  rlimcnp2  27112  efrlim  27115  muinv  27338  bposlem5  27433  lgsval2lem  27452  lgsval4  27462  lgsval4a  27464  lgsneg  27466  lgsneg1  27467  lgsdilem  27469  lgsdir  27477  lgsne0  27480  gausslemma2dlem1a  27510  gausslemma2dlem3  27513  2lgslem3  27549  2sqnn0  27583  rplogsumlem2  27630  dchrisum0fno1  27656  rplogsum  27672  pntrlog2bndlem4  27725  pntrlog2bndlem5  27726  padicabv  27775  ostth1  27778  ostth3  27783  expnnsval  28600  axlowdim  29292  vtxval  29331  iedgval  29332  funvtxdmge2val  29342  funiedgdmge2val  29343  funvtxdm2val  29344  funiedgdm2val  29345  snstrvtxval  29368  snstriedgval  29369  crctcshwlkn0lem3  30142  crctcsh  30154  clwlkclwwlklem2fv2  30328  eucrct2eupth  30577  fmptunsnop  33026  ccatws1f1o  33252  pmtridfv1  33396  pmtridfv2  33397  psgnfzto1stlem  33401  elrgspnlem2  33544  elrgspnlem3  33545  elrgspnlem4  33546  elrspunsn  33718  gsummoncoe1fzo  33868  mplasclco  33887  mplmulmvr  33910  evlextv  33913  psrmonmul  33921  esplyfval3  33943  esplyfval1  33944  esplyind  33946  extdgfialglem2  34064  rtelextdg2lem  34097  2sqr3minply  34151  cos9thpiminply  34159  smattr  34170  smatbl  34171  smatbr  34172  1smat1  34175  submatminr1  34181  madjusmdetlem1  34198  madjusmdetlem2  34199  xrge0iifcv  34305  xrge0iif1  34309  esumpinfval  34444  sigaclfu2  34492  eulerpartlemgs2  34751  ballotlemrv2  34893  signswmnd  34925  signswlid  34927  signsvtp  34951  signlem0  34955  ex-sategoelelomsuc  35899  ex-sategoelel12  35900  mrsubcn  35992  bcneg1  36209  bccolsum  36212  dfrdg2  36266  dfrdg4  36424  unblimceq0lem  37076  unbdqndv2lem2  37080  finxpreclem3  38020  finxpreclem5  38022  poimirlem1  38253  poimirlem2  38254  poimirlem7  38259  poimirlem10  38262  poimirlem11  38263  poimirlem16  38268  poimirlem17  38269  poimirlem20  38272  poimirlem24  38276  mblfinlem2  38290  itg2addnclem2  38304  ibladdnclem  38308  ftc1anclem6  38330  ftc1anclem8  38332  fdc  38377  heiborlem6  38448  cdleme31fv2  41148  cdlemefr27cl  41158  sticksstones10  42903  sticksstones12a  42905  sticksstones12  42906  evlsbagval  43301  fsuppssind  43308  mhpind  43309  prjspner1  43341  kelac1  43773  flcidc  43880  oe0suclim  43987  oe0rif  43995  cantnfub  44031  cantnfresb  44034  tfsconcatfv  44051  sqrtcval  44350  relexp01min  44422  relexpxpmin  44426  clsk1indlem0  44750  refsum2cnlem1  45740  upbdrech2  46010  ssfiunibd  46011  ioondisj2  46192  limsup10exlem  46469  icccncfext  46584  cncfiooicclem1  46590  cncfioobdlem  46593  dvnxpaek  46639  dvnprodlem1  46643  ditgeqiooicc  46657  iblcncfioo  46675  volioore  46687  dirkercncflem2  46801  dirkercncflem4  46803  fourierdlem40  46844  fourierdlem56  46859  fourierdlem65  46868  fourierdlem66  46869  fourierdlem73  46876  fourierdlem74  46877  fourierdlem75  46878  fourierdlem78  46881  fourierdlem79  46882  fourierdlem81  46884  fourierdlem82  46885  fourierdlem97  46900  fourierdlem103  46906  fourierdlem104  46907  sqwvfoura  46925  sqwvfourb  46926  fourierswlem  46927  fouriersw  46928  etransclem4  46935  etransclem14  46945  etransclem20  46951  etransclem22  46953  etransclem24  46955  etransclem25  46956  etransclem31  46962  etransclem32  46963  etransclem35  46966  sge0reval  47069  sge0sn  47076  nnfoctbdjlem  47152  isomenndlem  47227  ovnn0val  47248  ovnsubaddlem1  47267  hoidmvn0val  47281  hsphoidmvle2  47282  hsphoidmvle  47283  hoidmvval0  47284  hoidmv1lelem2  47289  hoidmvlelem2  47293  hoidmvlelem3  47294  ovnhoilem1  47298  hspmbllem1  47323  hspmbllem2  47324  volico2  47338  ovolval2lem  47340  ovnsubadd2lem  47342  ovolval4lem1  47346  ovnovollem3  47355  vonioo  47379  vonicc  47382  prproropf1olem3  48237  fdmdifeqresdif  49105  dig1  49371  dignn0flhalflem1  49378  itcoval1  49426  itcoval2  49427  itcoval3  49428  itcovalsuc  49430  ackvalsuc1mpt  49441