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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4483

This theorem is used by:  ifeqor  4534  ifnot  4535  ifan  4536  somincom  6128  partfun  6684  mpodifsnif  7533  tz7.44-2  8408  tz7.44-3  8409  unxpdomlem2  9241  sniffsupp  9385  unwdomg  9571  cantnfp1lem1  9672  cantnfp1lem3  9674  cantnflem1d  9682  ttrcltr  9710  updjudhcoinrg  10007  ttukeylem7  10586  canthp1lem2  10731  pwfseqlem3  10738  ind0  12323  xmulneg1  13392  rexmul  13394  xmulpnf1  13397  fzprval  13712  expnnval  14200  expneg  14205  tpf1ofv1  14635  tpf1ofv2  14636  ccatval2  14716  ccatalpha  14733  swrdnd  14797  swrdnd2  14798  swrd0  14801  swrdccatin2  14871  relexpsucnnr  15171  relexp1g  15172  sgnp  15236  sgnn  15240  absmax  15490  sumss2  15885  fsumsplit  15900  fprodntriv  16102  fprodsplit  16126  ef0lem  16237  rpnnen2lem9  16383  sadadd2lem2  16613  sadadd2  16623  eucalgf  16751  eucalginv  16752  eucalglt  16753  iserodd  17006  pcmpt  17063  pcmpt2  17064  ramtub  17183  prmo1  17208  fvprif  17726  gsumval2a  18867  mgm2nsgrplem2  19111  mgm2nsgrplem3  19112  sgrp2nmndlem3  19117  mulgnn  19278  mulgnegnn  19287  symgextfv  19625  pmtrprfv3  19661  pmtrdifellem4  19686  pmtrprfval  19694  pmtrprfvalrn  19695  odlem2  19746  dfod2  19771  gsumval3a  20110  gsumzsplit  20134  dmdprdsplitlem  20246  ablsimpgfind  20319  abvtrivd  21082  uvcvv0  22089  uvcff  22090  psrlidm  22262  psrridm  22263  mvrcl  22292  mplmon  22337  mplmonmul  22338  mplcoe1  22339  mplcoe5  22342  evlslem3  22382  selvvvval  22444  coe1tmfv2  22587  cply1coe0  22612  cply1coe0bi  22613  gsummoncoe1  22619  mulmarep1gsum1  22881  1marepvsma1  22891  mdetunilem2  22921  mdetunilem9  22928  maducoeval2  22948  symgmatr01lem  22961  gsummatr01lem3  22965  gsummatr01lem4  22966  gsummatr01  22967  m2cpm  23052  m2cpminvid2lem  23065  pmatcollpw3fi1lem1  23097  mp2pm2mplem4  23120  chfacffsupp  23167  chfacfscmul0  23169  chfacfpmmul0  23173  ptpjpre2  23892  ptopn2  23896  xkopt  23967  tsmssplit  24464  xrsxmet  25122  htpycc  25294  pco1  25329  pcohtpylem  25333  pcoass  25338  pcorevlem  25340  ovolunlem1a  25810  ovolunlem1  25811  ovolicc1  25830  itg11  26005  mbfi1flim  26037  itg2split  26063  itg2cnlem1  26075  itgeq2  26091  iblss  26118  itgss2  26126  itgss3  26128  itgless  26130  ibladdlem  26133  itgaddlem1  26136  itggt0  26157  itgcn  26158  dvexp2  26267  lhop2  26328  deg1add  26414  ig1pval3  26489  ply1termlem  26514  plyeq0lem  26522  plypf1  26524  dvply1  26598  pserdvlem2  26748  abelthlem9  26760  logtayllem  26980  logtayl  26981  cxpef  26986  rlimcnp2  27287  efrlim  27290  muinv  27513  bposlem5  27608  lgsval2lem  27627  lgsval4  27637  lgsval4a  27639  lgsneg  27641  lgsneg1  27642  lgsdilem  27644  lgsdir  27652  lgsne0  27655  gausslemma2dlem1a  27685  gausslemma2dlem3  27688  2lgslem3  27724  2sqnn0  27758  rplogsumlem2  27805  dchrisum0fno1  27831  rplogsum  27847  pntrlog2bndlem4  27900  pntrlog2bndlem5  27901  padicabv  27950  ostth1  27953  ostth3  27958  expnnsval  28805  angmgmaddov1  29381  axlowdim  29532  vtxval  29571  iedgval  29572  funvtxdmge2val  29582  funiedgdmge2val  29583  funvtxdm2val  29584  funiedgdm2val  29585  snstrvtxval  29608  snstriedgval  29609  crctcshwlkn0lem3  30394  crctcsh  30406  clwlkclwwlklem2fv2  30580  eucrct2eupth  30839  fmptunsnop  33286  ccatws1f1o  33507  pmtridfv1  33649  pmtridfv2  33650  psgnfzto1stlem  33654  elrgspnlem2  33797  elrgspnlem3  33798  elrgspnlem4  33799  elrspunsn  33972  gsummoncoe1fzo  34122  mplasclco  34141  mplmulmvr  34164  evlextv  34167  psrmonmul  34175  esplyfval3  34197  esplyfval1  34198  esplyind  34200  extdgfialglem2  34318  rtelextdg2lem  34351  2sqr3minply  34405  cos9thpiminply  34413  smattr  34424  smatbl  34425  smatbr  34426  1smat1  34429  submatminr1  34435  madjusmdetlem1  34452  madjusmdetlem2  34453  xrge0iifcv  34559  xrge0iif1  34563  esumpinfval  34698  sigaclfu2  34746  eulerpartlemgs2  35005  ballotlemrv2  35147  signswmnd  35179  signswlid  35181  signsvtp  35205  signlem0  35209  ex-sategoelelomsuc  36170  ex-sategoelel12  36171  mrsubcn  36263  bcneg1  36480  bccolsum  36483  dfrdg2  36537  dfrdg4  36695  unblimceq0lem  37352  unbdqndv2lem2  37356  finxpreclem3  38296  finxpreclem5  38298  poimirlem1  38519  poimirlem2  38520  poimirlem7  38525  poimirlem10  38528  poimirlem11  38529  poimirlem16  38534  poimirlem17  38535  poimirlem20  38538  poimirlem24  38542  mblfinlem2  38556  itg2addnclem2  38570  ibladdnclem  38574  ftc1anclem6  38596  ftc1anclem8  38598  fdc  38659  heiborlem6  38730  cdleme31fv2  41430  cdlemefr27cl  41440  sticksstones10  43185  sticksstones12a  43187  sticksstones12  43188  evlsbagval  43594  fsuppssind  43601  mhpind  43602  kelac1  44049  flcidc  44156  oe0suclim  44263  oe0rif  44271  cantnfub  44307  cantnfresb  44310  tfsconcatfv  44327  sqrtcval  44626  relexp01min  44698  relexpxpmin  44702  clsk1indlem0  45026  refsum2cnlem1  46023  upbdrech2  46293  ssfiunibd  46294  ioondisj2  46474  limsup10exlem  46751  icccncfext  46866  cncfiooicclem1  46872  cncfioobdlem  46875  dvnxpaek  46921  dvnprodlem1  46925  ditgeqiooicc  46939  iblcncfioo  46957  volioore  46969  dirkercncflem2  47083  dirkercncflem4  47085  fourierdlem40  47126  fourierdlem56  47141  fourierdlem65  47150  fourierdlem66  47151  fourierdlem73  47158  fourierdlem74  47159  fourierdlem75  47160  fourierdlem78  47163  fourierdlem79  47164  fourierdlem81  47166  fourierdlem82  47167  fourierdlem97  47182  fourierdlem103  47188  fourierdlem104  47189  sqwvfoura  47207  sqwvfourb  47208  fourierswlem  47209  fouriersw  47210  etransclem4  47217  etransclem14  47227  etransclem20  47233  etransclem22  47235  etransclem24  47237  etransclem25  47238  etransclem31  47244  etransclem32  47245  etransclem35  47248  sge0reval  47351  sge0sn  47358  nnfoctbdjlem  47434  isomenndlem  47509  ovnn0val  47530  ovnsubaddlem1  47549  hoidmvn0val  47563  hsphoidmvle2  47564  hsphoidmvle  47565  hoidmvval0  47566  hoidmv1lelem2  47571  hoidmvlelem2  47575  hoidmvlelem3  47576  ovnhoilem1  47580  hspmbllem1  47605  hspmbllem2  47606  volico2  47620  ovolval2lem  47622  ovnsubadd2lem  47624  ovolval4lem1  47628  ovnovollem3  47637  vonioo  47661  vonicc  47664  tmachlem-agreeprod  47916  tmachlem-tpopen  47920  prproropf1olem3  48556  fdmdifeqresdif  49423  dig1  49689  dignn0flhalflem1  49696  itcoval1  49744  itcoval2  49745  itcoval3  49746  itcovalsuc  49748  ackvalsuc1mpt  49759  crosspv2d  50930  crosspv3d  50931  veronesev1lem  50942  veronesev2lem  50943  veronesev3lem  50944  veronesev4lem  50945  veronesev5lem  50946  veronesev6lem  50947  veronesevrowd  50948