Theorem iffalsed 4486

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541  ifcif 4475

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-if 4476

This theorem is referenced by:  ifeqor  4527  ifnot  4528  ifan  4529  somincom  6081  partfun  6628  mpodifsnif  7461  tz7.44-2  8326  tz7.44-3  8327  unxpdomlem2  9141  sniffsupp  9284  unwdomg  9470  cantnfp1lem1  9568  cantnfp1lem3  9570  cantnflem1d  9578  ttrcltr  9606  updjudhcoinrg  9826  ttukeylem7  10406  canthp1lem2  10544  pwfseqlem3  10551  xmulneg1  13168  rexmul  13170  xmulpnf1  13173  fzprval  13485  expnnval  13971  expneg  13976  tpf1ofv1  14404  tpf1ofv2  14405  ccatval2  14485  ccatalpha  14501  swrdnd  14562  swrdnd2  14563  swrd0  14566  swrdccatin2  14636  relexpsucnnr  14932  relexp1g  14933  sgnp  14997  sgnn  15001  absmax  15237  sumss2  15633  fsumsplit  15648  fprodntriv  15849  fprodsplit  15873  ef0lem  15985  rpnnen2lem9  16131  sadadd2  16371  eucalgf  16494  eucalginv  16495  eucalglt  16496  iserodd  16747  pcmpt  16804  pcmpt2  16805  ramtub  16924  prmo1  16949  fvprif  17465  gsumval2a  18593  mgm2nsgrplem2  18827  mgm2nsgrplem3  18828  sgrp2nmndlem3  18833  mulgnn  18988  mulgnegnn  18997  symgextfv  19331  pmtrprfv3  19367  pmtrdifellem4  19392  pmtrprfval  19400  pmtrprfvalrn  19401  odlem2  19452  dfod2  19477  gsumval3a  19816  gsumzsplit  19840  dmdprdsplitlem  19952  ablsimpgfind  20025  abvtrivd  20748  uvcvv0  21728  uvcff  21729  psrlidm  21900  psrridm  21901  mvrcl  21930  mplmon  21971  mplmonmul  21972  mplcoe1  21973  mplcoe5  21976  evlslem3  22016  coe1tmfv2  22190  cply1coe0  22217  cply1coe0bi  22218  gsummoncoe1  22224  mulmarep1gsum1  22489  1marepvsma1  22499  mdetunilem2  22529  mdetunilem9  22536  maducoeval2  22556  symgmatr01lem  22569  gsummatr01lem3  22573  gsummatr01lem4  22574  gsummatr01  22575  m2cpm  22657  m2cpminvid2lem  22670  pmatcollpw3fi1lem1  22702  mp2pm2mplem4  22725  chfacffsupp  22772  chfacfscmul0  22774  chfacfpmmul0  22778  ptpjpre2  23496  ptopn2  23500  xkopt  23571  tsmssplit  24068  xrsxmet  24726  htpycc  24907  pco1  24943  pcohtpylem  24947  pcoass  24952  pcorevlem  24954  ovolunlem1a  25425  ovolunlem1  25426  ovolicc1  25445  itg11  25620  mbfi1flim  25652  itg2split  25678  itg2cnlem1  25690  itgeq2  25707  iblss  25734  itgss2  25742  itgss3  25744  itgless  25746  ibladdlem  25749  itgaddlem1  25752  itggt0  25773  itgcn  25774  dvexp2  25886  lhop2  25948  deg1add  26036  ig1pval3  26111  ply1termlem  26136  plyeq0lem  26143  plypf1  26145  dvply1  26219  pserdvlem2  26366  abelthlem9  26378  logtayllem  26596  logtayl  26597  cxpef  26602  rlimcnp2  26904  efrlim  26907  efrlimOLD  26908  muinv  27131  bposlem5  27227  lgsval2lem  27246  lgsval4  27256  lgsval4a  27258  lgsneg  27260  lgsneg1  27261  lgsdilem  27263  lgsdir  27271  lgsne0  27274  gausslemma2dlem1a  27304  gausslemma2dlem3  27307  2lgslem3  27343  2sqnn0  27377  rplogsumlem2  27424  dchrisum0fno1  27450  rplogsum  27466  pntrlog2bndlem4  27519  pntrlog2bndlem5  27520  padicabv  27569  ostth1  27572  ostth3  27577  expsnnval  28350  axlowdim  28940  vtxval  28979  iedgval  28980  funvtxdmge2val  28990  funiedgdmge2val  28991  funvtxdm2val  28992  funiedgdm2val  28993  snstrvtxval  29016  snstriedgval  29017  crctcshwlkn0lem3  29791  crctcsh  29803  clwlkclwwlklem2fv2  29974  eucrct2eupth  30223  fmptunsnop  32679  ind0  32837  ccatws1f1o  32930  pmtridfv1  33062  pmtridfv2  33063  psgnfzto1stlem  33067  elrgspnlem2  33208  elrgspnlem3  33209  elrgspnlem4  33210  elrspunsn  33392  gsummoncoe1fzo  33556  extdgfialglem2  33704  rtelextdg2lem  33737  2sqr3minply  33791  cos9thpiminply  33799  smattr  33810  smatbl  33811  smatbr  33812  1smat1  33815  submatminr1  33821  madjusmdetlem1  33838  madjusmdetlem2  33839  xrge0iifcv  33945  xrge0iif1  33949  esumpinfval  34084  sigaclfu2  34132  eulerpartlemgs2  34391  ballotlemrv2  34533  signswmnd  34568  signswlid  34570  signsvtp  34594  signlem0  34598  ex-sategoelelomsuc  35468  ex-sategoelel12  35469  mrsubcn  35561  bcneg1  35778  bccolsum  35781  dfrdg2  35835  dfrdg4  35991  unblimceq0lem  36546  unbdqndv2lem2  36550  finxpreclem3  37433  finxpreclem5  37435  poimirlem1  37667  poimirlem2  37668  poimirlem7  37673  poimirlem10  37676  poimirlem11  37677  poimirlem16  37682  poimirlem17  37683  poimirlem20  37686  poimirlem24  37690  mblfinlem2  37704  itg2addnclem2  37718  ibladdnclem  37722  ftc1anclem6  37744  ftc1anclem8  37746  fdc  37791  heiborlem6  37862  cdleme31fv2  40438  cdlemefr27cl  40448  sticksstones10  42194  sticksstones12a  42196  sticksstones12  42197  evlsbagval  42605  selvvvval  42624  fsuppssind  42632  mhpind  42633  prjspner1  42665  kelac1  43102  flcidc  43209  oe0suclim  43316  oe0rif  43324  cantnfub  43360  cantnfresb  43363  tfsconcatfv  43380  sqrtcval  43680  relexp01min  43752  relexpxpmin  43756  clsk1indlem0  44080  refsum2cnlem1  45080  upbdrech2  45355  ssfiunibd  45356  ioondisj2  45539  limsup10exlem  45816  icccncfext  45931  cncfiooicclem1  45937  cncfioobdlem  45940  dvnxpaek  45986  dvnprodlem1  45990  ditgeqiooicc  46004  iblcncfioo  46022  volioore  46034  dirkercncflem2  46148  dirkercncflem4  46150  fourierdlem40  46191  fourierdlem56  46206  fourierdlem65  46215  fourierdlem66  46216  fourierdlem73  46223  fourierdlem74  46224  fourierdlem75  46225  fourierdlem78  46228  fourierdlem79  46229  fourierdlem81  46231  fourierdlem82  46232  fourierdlem97  46247  fourierdlem103  46253  fourierdlem104  46254  sqwvfoura  46272  sqwvfourb  46273  fourierswlem  46274  fouriersw  46275  etransclem4  46282  etransclem14  46292  etransclem20  46298  etransclem22  46300  etransclem24  46302  etransclem25  46303  etransclem31  46309  etransclem32  46310  etransclem35  46313  sge0reval  46416  sge0sn  46423  nnfoctbdjlem  46499  isomenndlem  46574  ovnn0val  46595  ovnsubaddlem1  46614  hoidmvn0val  46628  hsphoidmvle2  46629  hsphoidmvle  46630  hoidmvval0  46631  hoidmv1lelem2  46636  hoidmvlelem2  46640  hoidmvlelem3  46641  ovnhoilem1  46645  hspmbllem1  46670  hspmbllem2  46671  volico2  46685  ovolval2lem  46687  ovnsubadd2lem  46689  ovolval4lem1  46693  ovnovollem3  46702  vonioo  46726  vonicc  46729  prproropf1olem3  47542  fdmdifeqresdif  48379  dig1  48646  dignn0flhalflem1  48653  itcoval1  48701  itcoval2  48702  itcoval3  48703  itcovalsuc  48705  ackvalsuc1mpt  48716