Theorem iffalsed 4488

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559  ifcif 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4478

This theorem is referenced by:  ifeqor  4529  ifnot  4530  ifan  4531  somincom  6116  partfun  6662  mpodifsnif  7505  tz7.44-2  8371  tz7.44-3  8372  unxpdomlem2  9194  sniffsupp  9339  unwdomg  9525  cantnfp1lem1  9626  cantnfp1lem3  9628  cantnflem1d  9636  ttrcltr  9664  updjudhcoinrg  9884  ttukeylem7  10465  canthp1lem2  10604  pwfseqlem3  10611  ind0  12198  xmulneg1  13265  rexmul  13267  xmulpnf1  13270  fzprval  13583  expnnval  14070  expneg  14075  tpf1ofv1  14503  tpf1ofv2  14504  ccatval2  14584  ccatalpha  14600  swrdnd  14661  swrdnd2  14662  swrd0  14665  swrdccatin2  14735  relexpsucnnr  15031  relexp1g  15032  sgnp  15096  sgnn  15100  absmax  15347  sumss2  15743  fsumsplit  15758  fprodntriv  15962  fprodsplit  15986  ef0lem  16098  rpnnen2lem9  16244  sadadd2  16484  eucalgf  16607  eucalginv  16608  eucalglt  16609  iserodd  16861  pcmpt  16918  pcmpt2  16919  ramtub  17038  prmo1  17063  fvprif  17581  gsumval2a  18709  mgm2nsgrplem2  18946  mgm2nsgrplem3  18947  sgrp2nmndlem3  18952  mulgnn  19107  mulgnegnn  19116  symgextfv  19448  pmtrprfv3  19484  pmtrdifellem4  19509  pmtrprfval  19517  pmtrprfvalrn  19518  odlem2  19569  dfod2  19594  gsumval3a  19933  gsumzsplit  19957  dmdprdsplitlem  20069  ablsimpgfind  20142  abvtrivd  20868  uvcvv0  21829  uvcff  21830  psrlidm  22000  psrridm  22001  mvrcl  22030  mplmon  22075  mplmonmul  22076  mplcoe1  22077  mplcoe5  22080  evlslem3  22120  selvvvval  22182  coe1tmfv2  22325  cply1coe0  22351  cply1coe0bi  22352  gsummoncoe1  22358  mulmarep1gsum1  22620  1marepvsma1  22630  mdetunilem2  22660  mdetunilem9  22667  maducoeval2  22687  symgmatr01lem  22700  gsummatr01lem3  22704  gsummatr01lem4  22705  gsummatr01  22706  m2cpm  22788  m2cpminvid2lem  22801  pmatcollpw3fi1lem1  22833  mp2pm2mplem4  22856  chfacffsupp  22903  chfacfscmul0  22905  chfacfpmmul0  22909  ptpjpre2  23627  ptopn2  23631  xkopt  23702  tsmssplit  24199  xrsxmet  24857  htpycc  25029  pco1  25064  pcohtpylem  25068  pcoass  25073  pcorevlem  25075  ovolunlem1a  25545  ovolunlem1  25546  ovolicc1  25565  itg11  25740  mbfi1flim  25772  itg2split  25798  itg2cnlem1  25810  itgeq2  25827  iblss  25854  itgss2  25862  itgss3  25864  itgless  25866  ibladdlem  25869  itgaddlem1  25872  itggt0  25893  itgcn  25894  dvexp2  26003  lhop2  26064  deg1add  26150  ig1pval3  26225  ply1termlem  26250  plyeq0lem  26257  plypf1  26259  dvply1  26335  pserdvlem2  26478  abelthlem9  26490  logtayllem  26711  logtayl  26712  cxpef  26717  rlimcnp2  27018  efrlim  27021  muinv  27244  bposlem5  27339  lgsval2lem  27358  lgsval4  27368  lgsval4a  27370  lgsneg  27372  lgsneg1  27373  lgsdilem  27375  lgsdir  27383  lgsne0  27386  gausslemma2dlem1a  27416  gausslemma2dlem3  27419  2lgslem3  27455  2sqnn0  27489  rplogsumlem2  27536  dchrisum0fno1  27562  rplogsum  27578  pntrlog2bndlem4  27631  pntrlog2bndlem5  27632  padicabv  27681  ostth1  27684  ostth3  27689  expnnsval  28506  axlowdim  29118  vtxval  29157  iedgval  29158  funvtxdmge2val  29168  funiedgdmge2val  29169  funvtxdm2val  29170  funiedgdm2val  29171  snstrvtxval  29194  snstriedgval  29195  crctcshwlkn0lem3  29968  crctcsh  29980  clwlkclwwlklem2fv2  30154  eucrct2eupth  30403  fmptunsnop  32862  ccatws1f1o  33089  pmtridfv1  33235  pmtridfv2  33236  psgnfzto1stlem  33240  elrgspnlem2  33384  elrgspnlem3  33385  elrgspnlem4  33386  elrspunsn  33575  gsummoncoe1fzo  33753  mplasclco  33773  mplmulmvr  33796  evlextv  33799  psrmonmul  33807  esplyfval3  33829  esplyfval1  33830  esplyind  33832  extdgfialglem2  33950  rtelextdg2lem  33983  2sqr3minply  34037  cos9thpiminply  34045  smattr  34056  smatbl  34057  smatbr  34058  1smat1  34061  submatminr1  34067  madjusmdetlem1  34084  madjusmdetlem2  34085  xrge0iifcv  34191  xrge0iif1  34195  esumpinfval  34330  sigaclfu2  34378  eulerpartlemgs2  34637  ballotlemrv2  34779  signswmnd  34811  signswlid  34813  signsvtp  34837  signlem0  34841  ex-sategoelelomsuc  35736  ex-sategoelel12  35737  mrsubcn  35829  bcneg1  36046  bccolsum  36049  dfrdg2  36103  dfrdg4  36261  unblimceq0lem  36904  unbdqndv2lem2  36908  finxpreclem3  37847  finxpreclem5  37849  poimirlem1  38080  poimirlem2  38081  poimirlem7  38086  poimirlem10  38089  poimirlem11  38090  poimirlem16  38095  poimirlem17  38096  poimirlem20  38099  poimirlem24  38103  mblfinlem2  38117  itg2addnclem2  38131  ibladdnclem  38135  ftc1anclem6  38157  ftc1anclem8  38159  fdc  38204  heiborlem6  38275  cdleme31fv2  40977  cdlemefr27cl  40987  sticksstones10  42732  sticksstones12a  42734  sticksstones12  42735  evlsbagval  43128  fsuppssind  43135  mhpind  43136  prjspner1  43168  kelac1  43600  flcidc  43707  oe0suclim  43814  oe0rif  43822  cantnfub  43858  cantnfresb  43861  tfsconcatfv  43878  sqrtcval  44177  relexp01min  44249  relexpxpmin  44253  clsk1indlem0  44577  refsum2cnlem1  45577  upbdrech2  45847  ssfiunibd  45848  ioondisj2  46029  limsup10exlem  46306  icccncfext  46421  cncfiooicclem1  46427  cncfioobdlem  46430  dvnxpaek  46476  dvnprodlem1  46480  ditgeqiooicc  46494  iblcncfioo  46512  volioore  46524  dirkercncflem2  46638  dirkercncflem4  46640  fourierdlem40  46681  fourierdlem56  46696  fourierdlem65  46705  fourierdlem66  46706  fourierdlem73  46713  fourierdlem74  46714  fourierdlem75  46715  fourierdlem78  46718  fourierdlem79  46719  fourierdlem81  46721  fourierdlem82  46722  fourierdlem97  46737  fourierdlem103  46743  fourierdlem104  46744  sqwvfoura  46762  sqwvfourb  46763  fourierswlem  46764  fouriersw  46765  etransclem4  46772  etransclem14  46782  etransclem20  46788  etransclem22  46790  etransclem24  46792  etransclem25  46793  etransclem31  46799  etransclem32  46800  etransclem35  46803  sge0reval  46906  sge0sn  46913  nnfoctbdjlem  46989  isomenndlem  47064  ovnn0val  47085  ovnsubaddlem1  47104  hoidmvn0val  47118  hsphoidmvle2  47119  hsphoidmvle  47120  hoidmvval0  47121  hoidmv1lelem2  47126  hoidmvlelem2  47130  hoidmvlelem3  47131  ovnhoilem1  47135  hspmbllem1  47160  hspmbllem2  47161  volico2  47175  ovolval2lem  47177  ovnsubadd2lem  47179  ovolval4lem1  47183  ovnovollem3  47192  vonioo  47216  vonicc  47219  prproropf1olem3  48071  fdmdifeqresdif  48924  dig1  49190  dignn0flhalflem1  49197  itcoval1  49245  itcoval2  49246  itcoval3  49247  itcovalsuc  49249  ackvalsuc1mpt  49260