Theorem iffalsed 4500

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570  ifcif 4489

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4490

This theorem is used by:  ifeqor  4541  ifnot  4542  ifan  4543  somincom  6136  partfun  6686  mpodifsnif  7531  tz7.44-2  8396  tz7.44-3  8397  unxpdomlem2  9220  sniffsupp  9363  unwdomg  9549  cantnfp1lem1  9650  cantnfp1lem3  9652  cantnflem1d  9660  ttrcltr  9688  updjudhcoinrg  9931  ttukeylem7  10510  canthp1lem2  10649  pwfseqlem3  10656  ind0  12239  xmulneg1  13306  rexmul  13308  xmulpnf1  13311  fzprval  13625  expnnval  14113  expneg  14118  tpf1ofv1  14547  tpf1ofv2  14548  ccatval2  14628  ccatalpha  14645  swrdnd  14709  swrdnd2  14710  swrd0  14713  swrdccatin2  14783  relexpsucnnr  15081  relexp1g  15082  sgnp  15146  sgnn  15150  absmax  15400  sumss2  15795  fsumsplit  15810  fprodntriv  16014  fprodsplit  16038  ef0lem  16149  rpnnen2lem9  16295  sadadd2lem2  16525  sadadd2  16535  eucalgf  16658  eucalginv  16659  eucalglt  16660  iserodd  16912  pcmpt  16969  pcmpt2  16970  ramtub  17089  prmo1  17114  fvprif  17632  gsumval2a  18764  mgm2nsgrplem2  19004  mgm2nsgrplem3  19005  sgrp2nmndlem3  19010  mulgnn  19164  mulgnegnn  19173  symgextfv  19511  pmtrprfv3  19547  pmtrdifellem4  19572  pmtrprfval  19580  pmtrprfvalrn  19581  odlem2  19632  dfod2  19657  gsumval3a  19996  gsumzsplit  20020  dmdprdsplitlem  20132  ablsimpgfind  20205  abvtrivd  20964  uvcvv0  21969  uvcff  21970  psrlidm  22140  psrridm  22141  mvrcl  22170  mplmon  22215  mplmonmul  22216  mplcoe1  22217  mplcoe5  22220  evlslem3  22260  selvvvval  22322  coe1tmfv2  22465  cply1coe0  22490  cply1coe0bi  22491  gsummoncoe1  22497  mulmarep1gsum1  22759  1marepvsma1  22769  mdetunilem2  22799  mdetunilem9  22806  maducoeval2  22826  symgmatr01lem  22839  gsummatr01lem3  22843  gsummatr01lem4  22844  gsummatr01  22845  m2cpm  22927  m2cpminvid2lem  22940  pmatcollpw3fi1lem1  22972  mp2pm2mplem4  22995  chfacffsupp  23042  chfacfscmul0  23044  chfacfpmmul0  23048  ptpjpre2  23766  ptopn2  23770  xkopt  23841  tsmssplit  24338  xrsxmet  24996  htpycc  25168  pco1  25203  pcohtpylem  25207  pcoass  25212  pcorevlem  25214  ovolunlem1a  25684  ovolunlem1  25685  ovolicc1  25704  itg11  25879  mbfi1flim  25911  itg2split  25937  itg2cnlem1  25949  itgeq2  25966  iblss  25993  itgss2  26001  itgss3  26003  itgless  26005  ibladdlem  26008  itgaddlem1  26011  itggt0  26032  itgcn  26033  dvexp2  26142  lhop2  26203  deg1add  26289  ig1pval3  26364  ply1termlem  26389  plyeq0lem  26396  plypf1  26398  dvply1  26474  pserdvlem2  26620  abelthlem9  26632  logtayllem  26853  logtayl  26854  cxpef  26859  rlimcnp2  27160  efrlim  27163  muinv  27386  bposlem5  27481  lgsval2lem  27500  lgsval4  27510  lgsval4a  27512  lgsneg  27514  lgsneg1  27515  lgsdilem  27517  lgsdir  27525  lgsne0  27528  gausslemma2dlem1a  27558  gausslemma2dlem3  27561  2lgslem3  27597  2sqnn0  27631  rplogsumlem2  27678  dchrisum0fno1  27704  rplogsum  27720  pntrlog2bndlem4  27773  pntrlog2bndlem5  27774  padicabv  27823  ostth1  27826  ostth3  27831  expnnsval  28648  axlowdim  29340  vtxval  29379  iedgval  29380  funvtxdmge2val  29390  funiedgdmge2val  29391  funvtxdm2val  29392  funiedgdm2val  29393  snstrvtxval  29416  snstriedgval  29417  crctcshwlkn0lem3  30190  crctcsh  30202  clwlkclwwlklem2fv2  30376  eucrct2eupth  30625  fmptunsnop  33074  ccatws1f1o  33296  pmtridfv1  33438  pmtridfv2  33439  psgnfzto1stlem  33443  elrgspnlem2  33586  elrgspnlem3  33587  elrgspnlem4  33588  elrspunsn  33760  gsummoncoe1fzo  33910  mplasclco  33929  mplmulmvr  33952  evlextv  33955  psrmonmul  33963  esplyfval3  33985  esplyfval1  33986  esplyind  33988  extdgfialglem2  34106  rtelextdg2lem  34139  2sqr3minply  34193  cos9thpiminply  34201  smattr  34212  smatbl  34213  smatbr  34214  1smat1  34217  submatminr1  34223  madjusmdetlem1  34240  madjusmdetlem2  34241  xrge0iifcv  34347  xrge0iif1  34351  esumpinfval  34486  sigaclfu2  34534  eulerpartlemgs2  34794  ballotlemrv2  34936  signswmnd  34968  signswlid  34970  signsvtp  34994  signlem0  34998  ex-sategoelelomsuc  35931  ex-sategoelel12  35932  mrsubcn  36024  bcneg1  36241  bccolsum  36244  dfrdg2  36298  dfrdg4  36456  unblimceq0lem  37128  unbdqndv2lem2  37132  finxpreclem3  38072  finxpreclem5  38074  poimirlem1  38305  poimirlem2  38306  poimirlem7  38311  poimirlem10  38314  poimirlem11  38315  poimirlem16  38320  poimirlem17  38321  poimirlem20  38324  poimirlem24  38328  mblfinlem2  38342  itg2addnclem2  38356  ibladdnclem  38360  ftc1anclem6  38382  ftc1anclem8  38384  fdc  38429  heiborlem6  38500  cdleme31fv2  41200  cdlemefr27cl  41210  sticksstones10  42955  sticksstones12a  42957  sticksstones12  42958  evlsbagval  43351  fsuppssind  43358  mhpind  43359  prjspner1  43391  kelac1  43823  flcidc  43930  oe0suclim  44037  oe0rif  44045  cantnfub  44081  cantnfresb  44084  tfsconcatfv  44101  sqrtcval  44400  relexp01min  44472  relexpxpmin  44476  clsk1indlem0  44800  refsum2cnlem1  45790  upbdrech2  46060  ssfiunibd  46061  ioondisj2  46242  limsup10exlem  46519  icccncfext  46634  cncfiooicclem1  46640  cncfioobdlem  46643  dvnxpaek  46689  dvnprodlem1  46693  ditgeqiooicc  46707  iblcncfioo  46725  volioore  46737  dirkercncflem2  46851  dirkercncflem4  46853  fourierdlem40  46894  fourierdlem56  46909  fourierdlem65  46918  fourierdlem66  46919  fourierdlem73  46926  fourierdlem74  46927  fourierdlem75  46928  fourierdlem78  46931  fourierdlem79  46932  fourierdlem81  46934  fourierdlem82  46935  fourierdlem97  46950  fourierdlem103  46956  fourierdlem104  46957  sqwvfoura  46975  sqwvfourb  46976  fourierswlem  46977  fouriersw  46978  etransclem4  46985  etransclem14  46995  etransclem20  47001  etransclem22  47003  etransclem24  47005  etransclem25  47006  etransclem31  47012  etransclem32  47013  etransclem35  47016  sge0reval  47119  sge0sn  47126  nnfoctbdjlem  47202  isomenndlem  47277  ovnn0val  47298  ovnsubaddlem1  47317  hoidmvn0val  47331  hsphoidmvle2  47332  hsphoidmvle  47333  hoidmvval0  47334  hoidmv1lelem2  47339  hoidmvlelem2  47343  hoidmvlelem3  47344  ovnhoilem1  47348  hspmbllem1  47373  hspmbllem2  47374  volico2  47388  ovolval2lem  47390  ovnsubadd2lem  47392  ovolval4lem1  47396  ovnovollem3  47405  vonioo  47429  vonicc  47432  prproropf1olem3  48287  fdmdifeqresdif  49155  dig1  49421  dignn0flhalflem1  49428  itcoval1  49476  itcoval2  49477  itcoval3  49478  itcovalsuc  49480  ackvalsuc1mpt  49491  crosspv2i  50676  crosspv3i  50677