Theorem iffalsed 4478

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  ifeqor  4519  ifnot  4520  ifan  4521  somincom  6091  partfun  6639  mpodifsnif  7475  tz7.44-2  8339  tz7.44-3  8340  unxpdomlem2  9160  sniffsupp  9306  unwdomg  9492  cantnfp1lem1  9590  cantnfp1lem3  9592  cantnflem1d  9600  ttrcltr  9628  updjudhcoinrg  9848  ttukeylem7  10428  canthp1lem2  10567  pwfseqlem3  10574  ind0  12160  xmulneg1  13212  rexmul  13214  xmulpnf1  13217  fzprval  13530  expnnval  14017  expneg  14022  tpf1ofv1  14450  tpf1ofv2  14451  ccatval2  14531  ccatalpha  14547  swrdnd  14608  swrdnd2  14609  swrd0  14612  swrdccatin2  14682  relexpsucnnr  14978  relexp1g  14979  sgnp  15043  sgnn  15047  absmax  15283  sumss2  15679  fsumsplit  15694  fprodntriv  15898  fprodsplit  15922  ef0lem  16034  rpnnen2lem9  16180  sadadd2  16420  eucalgf  16543  eucalginv  16544  eucalglt  16545  iserodd  16797  pcmpt  16854  pcmpt2  16855  ramtub  16974  prmo1  16999  fvprif  17516  gsumval2a  18644  mgm2nsgrplem2  18881  mgm2nsgrplem3  18882  sgrp2nmndlem3  18887  mulgnn  19042  mulgnegnn  19051  symgextfv  19384  pmtrprfv3  19420  pmtrdifellem4  19445  pmtrprfval  19453  pmtrprfvalrn  19454  odlem2  19505  dfod2  19530  gsumval3a  19869  gsumzsplit  19893  dmdprdsplitlem  20005  ablsimpgfind  20078  abvtrivd  20800  uvcvv0  21780  uvcff  21781  psrlidm  21950  psrridm  21951  mvrcl  21980  mplmon  22023  mplmonmul  22024  mplcoe1  22025  mplcoe5  22028  evlslem3  22068  coe1tmfv2  22250  cply1coe0  22276  cply1coe0bi  22277  gsummoncoe1  22283  mulmarep1gsum1  22548  1marepvsma1  22558  mdetunilem2  22588  mdetunilem9  22595  maducoeval2  22615  symgmatr01lem  22628  gsummatr01lem3  22632  gsummatr01lem4  22633  gsummatr01  22634  m2cpm  22716  m2cpminvid2lem  22729  pmatcollpw3fi1lem1  22761  mp2pm2mplem4  22784  chfacffsupp  22831  chfacfscmul0  22833  chfacfpmmul0  22837  ptpjpre2  23555  ptopn2  23559  xkopt  23630  tsmssplit  24127  xrsxmet  24785  htpycc  24957  pco1  24992  pcohtpylem  24996  pcoass  25001  pcorevlem  25003  ovolunlem1a  25473  ovolunlem1  25474  ovolicc1  25493  itg11  25668  mbfi1flim  25700  itg2split  25726  itg2cnlem1  25738  itgeq2  25755  iblss  25782  itgss2  25790  itgss3  25792  itgless  25794  ibladdlem  25797  itgaddlem1  25800  itggt0  25821  itgcn  25822  dvexp2  25931  lhop2  25992  deg1add  26078  ig1pval3  26153  ply1termlem  26178  plyeq0lem  26185  plypf1  26187  dvply1  26260  pserdvlem2  26406  abelthlem9  26418  logtayllem  26636  logtayl  26637  cxpef  26642  rlimcnp2  26943  efrlim  26946  efrlimOLD  26947  muinv  27170  bposlem5  27265  lgsval2lem  27284  lgsval4  27294  lgsval4a  27296  lgsneg  27298  lgsneg1  27299  lgsdilem  27301  lgsdir  27309  lgsne0  27312  gausslemma2dlem1a  27342  gausslemma2dlem3  27345  2lgslem3  27381  2sqnn0  27415  rplogsumlem2  27462  dchrisum0fno1  27488  rplogsum  27504  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  padicabv  27607  ostth1  27610  ostth3  27615  expnnsval  28432  axlowdim  29044  vtxval  29083  iedgval  29084  funvtxdmge2val  29094  funiedgdmge2val  29095  funvtxdm2val  29096  funiedgdm2val  29097  snstrvtxval  29120  snstriedgval  29121  crctcshwlkn0lem3  29895  crctcsh  29907  clwlkclwwlklem2fv2  30081  eucrct2eupth  30330  fmptunsnop  32788  ccatws1f1o  33026  pmtridfv1  33171  pmtridfv2  33172  psgnfzto1stlem  33176  elrgspnlem2  33319  elrgspnlem3  33320  elrgspnlem4  33321  elrspunsn  33504  gsummoncoe1fzo  33672  mplmulmvr  33698  evlextv  33701  psrmonmul  33709  esplyfval3  33731  esplyfval1  33732  esplyind  33734  extdgfialglem2  33853  rtelextdg2lem  33886  2sqr3minply  33940  cos9thpiminply  33948  smattr  33959  smatbl  33960  smatbr  33961  1smat1  33964  submatminr1  33970  madjusmdetlem1  33987  madjusmdetlem2  33988  xrge0iifcv  34094  xrge0iif1  34098  esumpinfval  34233  sigaclfu2  34281  eulerpartlemgs2  34540  ballotlemrv2  34682  signswmnd  34717  signswlid  34719  signsvtp  34743  signlem0  34747  ex-sategoelelomsuc  35624  ex-sategoelel12  35625  mrsubcn  35717  bcneg1  35934  bccolsum  35937  dfrdg2  35991  dfrdg4  36149  unblimceq0lem  36782  unbdqndv2lem2  36786  finxpreclem3  37723  finxpreclem5  37725  poimirlem1  37956  poimirlem2  37957  poimirlem7  37962  poimirlem10  37965  poimirlem11  37966  poimirlem16  37971  poimirlem17  37972  poimirlem20  37975  poimirlem24  37979  mblfinlem2  37993  itg2addnclem2  38007  ibladdnclem  38011  ftc1anclem6  38033  ftc1anclem8  38035  fdc  38080  heiborlem6  38151  cdleme31fv2  40853  cdlemefr27cl  40863  sticksstones10  42608  sticksstones12a  42610  sticksstones12  42611  evlsbagval  43016  selvvvval  43032  fsuppssind  43040  mhpind  43041  prjspner1  43073  kelac1  43509  flcidc  43616  oe0suclim  43723  oe0rif  43731  cantnfub  43767  cantnfresb  43770  tfsconcatfv  43787  sqrtcval  44086  relexp01min  44158  relexpxpmin  44162  clsk1indlem0  44486  refsum2cnlem1  45486  upbdrech2  45759  ssfiunibd  45760  ioondisj2  45941  limsup10exlem  46218  icccncfext  46333  cncfiooicclem1  46339  cncfioobdlem  46342  dvnxpaek  46388  dvnprodlem1  46392  ditgeqiooicc  46406  iblcncfioo  46424  volioore  46436  dirkercncflem2  46550  dirkercncflem4  46552  fourierdlem40  46593  fourierdlem56  46608  fourierdlem65  46617  fourierdlem66  46618  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem78  46630  fourierdlem79  46631  fourierdlem81  46633  fourierdlem82  46634  fourierdlem97  46649  fourierdlem103  46655  fourierdlem104  46656  sqwvfoura  46674  sqwvfourb  46675  fourierswlem  46676  fouriersw  46677  etransclem4  46684  etransclem14  46694  etransclem20  46700  etransclem22  46702  etransclem24  46704  etransclem25  46705  etransclem31  46711  etransclem32  46712  etransclem35  46715  sge0reval  46818  sge0sn  46825  nnfoctbdjlem  46901  isomenndlem  46976  ovnn0val  46997  ovnsubaddlem1  47016  hoidmvn0val  47030  hsphoidmvle2  47031  hsphoidmvle  47032  hoidmvval0  47033  hoidmv1lelem2  47038  hoidmvlelem2  47042  hoidmvlelem3  47043  ovnhoilem1  47047  hspmbllem1  47072  hspmbllem2  47073  volico2  47087  ovolval2lem  47089  ovnsubadd2lem  47091  ovolval4lem1  47095  ovnovollem3  47104  vonioo  47128  vonicc  47131  prproropf1olem3  47977  fdmdifeqresdif  48830  dig1  49096  dignn0flhalflem1  49103  itcoval1  49151  itcoval2  49152  itcoval3  49153  itcovalsuc  49155  ackvalsuc1mpt  49166