Theorem iffalsed 4477

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4467

This theorem is referenced by:  ifeqor  4518  ifnot  4519  ifan  4520  somincom  6097  partfun  6645  mpodifsnif  7482  tz7.44-2  8346  tz7.44-3  8347  unxpdomlem2  9167  sniffsupp  9313  unwdomg  9499  cantnfp1lem1  9599  cantnfp1lem3  9601  cantnflem1d  9609  ttrcltr  9637  updjudhcoinrg  9857  ttukeylem7  10437  canthp1lem2  10576  pwfseqlem3  10583  ind0  12169  xmulneg1  13221  rexmul  13223  xmulpnf1  13226  fzprval  13539  expnnval  14026  expneg  14031  tpf1ofv1  14459  tpf1ofv2  14460  ccatval2  14540  ccatalpha  14556  swrdnd  14617  swrdnd2  14618  swrd0  14621  swrdccatin2  14691  relexpsucnnr  14987  relexp1g  14988  sgnp  15052  sgnn  15056  absmax  15292  sumss2  15688  fsumsplit  15703  fprodntriv  15907  fprodsplit  15931  ef0lem  16043  rpnnen2lem9  16189  sadadd2  16429  eucalgf  16552  eucalginv  16553  eucalglt  16554  iserodd  16806  pcmpt  16863  pcmpt2  16864  ramtub  16983  prmo1  17008  fvprif  17525  gsumval2a  18653  mgm2nsgrplem2  18890  mgm2nsgrplem3  18891  sgrp2nmndlem3  18896  mulgnn  19051  mulgnegnn  19060  symgextfv  19393  pmtrprfv3  19429  pmtrdifellem4  19454  pmtrprfval  19462  pmtrprfvalrn  19463  odlem2  19514  dfod2  19539  gsumval3a  19878  gsumzsplit  19902  dmdprdsplitlem  20014  ablsimpgfind  20087  abvtrivd  20809  uvcvv0  21770  uvcff  21771  psrlidm  21940  psrridm  21941  mvrcl  21970  mplmon  22013  mplmonmul  22014  mplcoe1  22015  mplcoe5  22018  evlslem3  22058  coe1tmfv2  22240  cply1coe0  22266  cply1coe0bi  22267  gsummoncoe1  22273  mulmarep1gsum1  22538  1marepvsma1  22548  mdetunilem2  22578  mdetunilem9  22585  maducoeval2  22605  symgmatr01lem  22618  gsummatr01lem3  22622  gsummatr01lem4  22623  gsummatr01  22624  m2cpm  22706  m2cpminvid2lem  22719  pmatcollpw3fi1lem1  22751  mp2pm2mplem4  22774  chfacffsupp  22821  chfacfscmul0  22823  chfacfpmmul0  22827  ptpjpre2  23545  ptopn2  23549  xkopt  23620  tsmssplit  24117  xrsxmet  24775  htpycc  24947  pco1  24982  pcohtpylem  24986  pcoass  24991  pcorevlem  24993  ovolunlem1a  25463  ovolunlem1  25464  ovolicc1  25483  itg11  25658  mbfi1flim  25690  itg2split  25716  itg2cnlem1  25728  itgeq2  25745  iblss  25772  itgss2  25780  itgss3  25782  itgless  25784  ibladdlem  25787  itgaddlem1  25790  itggt0  25811  itgcn  25812  dvexp2  25921  lhop2  25982  deg1add  26068  ig1pval3  26143  ply1termlem  26168  plyeq0lem  26175  plypf1  26177  dvply1  26250  pserdvlem2  26393  abelthlem9  26405  logtayllem  26623  logtayl  26624  cxpef  26629  rlimcnp2  26930  efrlim  26933  muinv  27156  bposlem5  27251  lgsval2lem  27270  lgsval4  27280  lgsval4a  27282  lgsneg  27284  lgsneg1  27285  lgsdilem  27287  lgsdir  27295  lgsne0  27298  gausslemma2dlem1a  27328  gausslemma2dlem3  27331  2lgslem3  27367  2sqnn0  27401  rplogsumlem2  27448  dchrisum0fno1  27474  rplogsum  27490  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  padicabv  27593  ostth1  27596  ostth3  27601  expnnsval  28418  axlowdim  29030  vtxval  29069  iedgval  29070  funvtxdmge2val  29080  funiedgdmge2val  29081  funvtxdm2val  29082  funiedgdm2val  29083  snstrvtxval  29106  snstriedgval  29107  crctcshwlkn0lem3  29880  crctcsh  29892  clwlkclwwlklem2fv2  30066  eucrct2eupth  30315  fmptunsnop  32773  ccatws1f1o  33011  pmtridfv1  33156  pmtridfv2  33157  psgnfzto1stlem  33161  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  elrspunsn  33489  gsummoncoe1fzo  33657  mplmulmvr  33683  evlextv  33686  psrmonmul  33694  esplyfval3  33716  esplyfval1  33717  esplyind  33719  extdgfialglem2  33837  rtelextdg2lem  33870  2sqr3minply  33924  cos9thpiminply  33932  smattr  33943  smatbl  33944  smatbr  33945  1smat1  33948  submatminr1  33954  madjusmdetlem1  33971  madjusmdetlem2  33972  xrge0iifcv  34078  xrge0iif1  34082  esumpinfval  34217  sigaclfu2  34265  eulerpartlemgs2  34524  ballotlemrv2  34666  signswmnd  34701  signswlid  34703  signsvtp  34727  signlem0  34731  ex-sategoelelomsuc  35608  ex-sategoelel12  35609  mrsubcn  35701  bcneg1  35918  bccolsum  35921  dfrdg2  35975  dfrdg4  36133  unblimceq0lem  36766  unbdqndv2lem2  36770  finxpreclem3  37709  finxpreclem5  37711  poimirlem1  37942  poimirlem2  37943  poimirlem7  37948  poimirlem10  37951  poimirlem11  37952  poimirlem16  37957  poimirlem17  37958  poimirlem20  37961  poimirlem24  37965  mblfinlem2  37979  itg2addnclem2  37993  ibladdnclem  37997  ftc1anclem6  38019  ftc1anclem8  38021  fdc  38066  heiborlem6  38137  cdleme31fv2  40839  cdlemefr27cl  40849  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  evlsbagval  43002  selvvvval  43018  fsuppssind  43026  mhpind  43027  prjspner1  43059  kelac1  43491  flcidc  43598  oe0suclim  43705  oe0rif  43713  cantnfub  43749  cantnfresb  43752  tfsconcatfv  43769  sqrtcval  44068  relexp01min  44140  relexpxpmin  44144  clsk1indlem0  44468  refsum2cnlem1  45468  upbdrech2  45741  ssfiunibd  45742  ioondisj2  45923  limsup10exlem  46200  icccncfext  46315  cncfiooicclem1  46321  cncfioobdlem  46324  dvnxpaek  46370  dvnprodlem1  46374  ditgeqiooicc  46388  iblcncfioo  46406  volioore  46418  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem40  46575  fourierdlem56  46590  fourierdlem65  46599  fourierdlem66  46600  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem78  46612  fourierdlem79  46613  fourierdlem81  46615  fourierdlem82  46616  fourierdlem97  46631  fourierdlem103  46637  fourierdlem104  46638  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  etransclem4  46666  etransclem14  46676  etransclem20  46682  etransclem22  46684  etransclem24  46686  etransclem25  46687  etransclem31  46693  etransclem32  46694  etransclem35  46697  sge0reval  46800  sge0sn  46807  nnfoctbdjlem  46883  isomenndlem  46958  ovnn0val  46979  ovnsubaddlem1  46998  hoidmvn0val  47012  hsphoidmvle2  47013  hsphoidmvle  47014  hoidmvval0  47015  hoidmv1lelem2  47020  hoidmvlelem2  47024  hoidmvlelem3  47025  ovnhoilem1  47029  hspmbllem1  47054  hspmbllem2  47055  volico2  47069  ovolval2lem  47071  ovnsubadd2lem  47073  ovolval4lem1  47077  ovnovollem3  47086  vonioo  47110  vonicc  47113  prproropf1olem3  47965  fdmdifeqresdif  48818  dig1  49084  dignn0flhalflem1  49091  itcoval1  49139  itcoval2  49140  itcoval3  49141  itcovalsuc  49143  ackvalsuc1mpt  49154