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 1537  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4468

This theorem is referenced by:  ifeqor  4516  ifnot  4517  ifan  4518  somincom  5994  mpodifsnif  7267  tz7.44-2  8043  tz7.44-3  8044  unxpdomlem2  8723  sniffsupp  8873  unwdomg  9048  cantnfp1lem1  9141  cantnfp1lem3  9143  cantnflem1d  9151  updjudhcoinrg  9362  ttukeylem7  9937  canthp1lem2  10075  pwfseqlem3  10082  xmulneg1  12663  rexmul  12665  xmulpnf1  12668  fzprval  12969  expnnval  13433  expneg  13438  ccatval2  13932  ccatalpha  13947  swrdnd  14016  swrdnd2  14017  swrd0  14020  swrdccatin2  14091  relexpsucnnr  14384  relexp1g  14385  sgnp  14449  sgnn  14453  absmax  14689  sumss2  15083  fsumsplit  15097  fprodntriv  15296  fprodsplit  15320  ef0lem  15432  rpnnen2lem9  15575  sadadd2  15809  eucalgf  15927  eucalginv  15928  eucalglt  15929  iserodd  16172  pcmpt  16228  pcmpt2  16229  ramtub  16348  prmo1  16373  fvprif  16834  gsumval2a  17895  mgm2nsgrplem2  18084  mgm2nsgrplem3  18085  sgrp2nmndlem3  18090  mulgnn  18232  mulgnegnn  18238  symgextfv  18546  pmtrprfv3  18582  pmtrdifellem4  18607  pmtrprfval  18615  pmtrprfvalrn  18616  odlem2  18667  dfod2  18691  gsumval3a  19023  gsumzsplit  19047  dmdprdsplitlem  19159  ablsimpgfind  19232  abvtrivd  19611  psrlidm  20183  psrridm  20184  mvrcl  20229  mplmon  20244  mplmonmul  20245  mplcoe1  20246  mplcoe5  20249  evlslem3  20293  coe1tmfv2  20443  cply1coe0  20467  cply1coe0bi  20468  gsummoncoe1  20472  uvcvv0  20934  uvcff  20935  mulmarep1gsum1  21182  1marepvsma1  21192  mdetunilem2  21222  mdetunilem9  21229  maducoeval2  21249  symgmatr01lem  21262  gsummatr01lem3  21266  gsummatr01lem4  21267  gsummatr01  21268  m2cpm  21349  m2cpminvid2lem  21362  pmatcollpw3fi1lem1  21394  mp2pm2mplem4  21417  chfacffsupp  21464  chfacfscmul0  21466  chfacfpmmul0  21470  ptpjpre2  22188  ptopn2  22192  xkopt  22263  tsmssplit  22760  xrsxmet  23417  htpycc  23584  pco1  23619  pcohtpylem  23623  pcoass  23628  pcorevlem  23630  ovolunlem1a  24097  ovolunlem1  24098  ovolicc1  24117  itg11  24292  mbfi1flim  24324  itg2split  24350  itg2cnlem1  24362  itgeq2  24378  iblss  24405  itgss2  24413  itgss3  24415  itgless  24417  ibladdlem  24420  itgaddlem1  24423  itggt0  24442  itgcn  24443  dvexp2  24551  lhop2  24612  deg1add  24697  ig1pval3  24768  ply1termlem  24793  plyeq0lem  24800  plypf1  24802  dvply1  24873  pserdvlem2  25016  abelthlem9  25028  logtayllem  25242  logtayl  25243  cxpef  25248  rlimcnp2  25544  efrlim  25547  muinv  25770  bposlem5  25864  lgsval2lem  25883  lgsval4  25893  lgsval4a  25895  lgsneg  25897  lgsneg1  25898  lgsdilem  25900  lgsdir  25908  lgsne0  25911  gausslemma2dlem1a  25941  gausslemma2dlem3  25944  2lgslem3  25980  2sqnn0  26014  rplogsumlem2  26061  dchrisum0fno1  26087  rplogsum  26103  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  padicabv  26206  ostth1  26209  ostth3  26214  axlowdim  26747  vtxval  26785  iedgval  26786  funvtxdmge2val  26796  funiedgdmge2val  26797  funvtxdm2val  26798  funiedgdm2val  26799  snstrvtxval  26822  snstriedgval  26823  crctcshwlkn0lem3  27590  crctcsh  27602  clwlkclwwlklem2fv2  27774  eucrct2eupth  28024  partfun  30421  pmtridfv1  30737  pmtridfv2  30738  psgnfzto1stlem  30742  smattr  31064  smatbl  31065  smatbr  31066  1smat1  31069  submatminr1  31075  madjusmdetlem1  31092  madjusmdetlem2  31093  xrge0iifcv  31177  xrge0iif1  31181  ind0  31277  esumpinfval  31332  sigaclfu2  31380  eulerpartlemgs2  31638  ballotlemrv2  31779  signswmnd  31827  signswlid  31829  signsvtp  31853  signlem0  31857  ex-sategoelelomsuc  32673  ex-sategoelel12  32674  mrsubcn  32766  bcneg1  32968  bccolsum  32971  dfrdg2  33040  dfrdg4  33412  unblimceq0lem  33845  unbdqndv2lem2  33849  finxpreclem3  34677  finxpreclem5  34679  poimirlem1  34908  poimirlem2  34909  poimirlem7  34914  poimirlem10  34917  poimirlem11  34918  poimirlem16  34923  poimirlem17  34924  poimirlem20  34927  poimirlem24  34931  mblfinlem2  34945  itg2addnclem2  34959  ibladdnclem  34963  ftc1anclem6  34987  ftc1anclem8  34989  fdc  35035  heiborlem6  35109  cdleme31fv2  37544  cdlemefr27cl  37554  kelac1  39683  flcidc  39794  relexp01min  40078  relexpxpmin  40082  clsk1indlem0  40411  refsum2cnlem1  41314  upbdrech2  41595  ssfiunibd  41596  ioondisj2  41787  limsup10exlem  42073  icccncfext  42190  cncfiooicclem1  42196  cncfioobdlem  42199  dvnxpaek  42247  dvnprodlem1  42251  ditgeqiooicc  42265  iblcncfioo  42283  volioore  42295  dirkercncflem2  42409  dirkercncflem4  42411  fourierdlem40  42452  fourierdlem56  42467  fourierdlem65  42476  fourierdlem66  42477  fourierdlem73  42484  fourierdlem74  42485  fourierdlem75  42486  fourierdlem78  42489  fourierdlem79  42490  fourierdlem81  42492  fourierdlem82  42493  fourierdlem97  42508  fourierdlem103  42514  fourierdlem104  42515  sqwvfoura  42533  sqwvfourb  42534  fourierswlem  42535  fouriersw  42536  etransclem4  42543  etransclem14  42553  etransclem20  42559  etransclem22  42561  etransclem24  42563  etransclem25  42564  etransclem31  42570  etransclem32  42571  etransclem35  42574  sge0reval  42674  sge0sn  42681  nnfoctbdjlem  42757  isomenndlem  42832  ovnn0val  42853  ovnsubaddlem1  42872  hoidmvn0val  42886  hsphoidmvle2  42887  hsphoidmvle  42888  hoidmvval0  42889  hoidmv1lelem2  42894  hoidmvlelem2  42898  hoidmvlelem3  42899  ovnhoilem1  42903  hspmbllem1  42928  hspmbllem2  42929  volico2  42943  ovolval2lem  42945  ovnsubadd2lem  42947  ovolval4lem1  42951  ovnovollem3  42960  vonioo  42984  vonicc  42987  prproropf1olem3  43687  fdmdifeqresdif  44410  dig1  44688  dignn0flhalflem1  44695