Theorem iffalsed 4492

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4482

This theorem is referenced by:  ifeqor  4533  ifnot  4534  ifan  4535  somincom  6099  partfun  6647  mpodifsnif  7483  tz7.44-2  8348  tz7.44-3  8349  unxpdomlem2  9169  sniffsupp  9315  unwdomg  9501  cantnfp1lem1  9599  cantnfp1lem3  9601  cantnflem1d  9609  ttrcltr  9637  updjudhcoinrg  9857  ttukeylem7  10437  canthp1lem2  10576  pwfseqlem3  10583  xmulneg1  13196  rexmul  13198  xmulpnf1  13201  fzprval  13513  expnnval  13999  expneg  14004  tpf1ofv1  14432  tpf1ofv2  14433  ccatval2  14513  ccatalpha  14529  swrdnd  14590  swrdnd2  14591  swrd0  14594  swrdccatin2  14664  relexpsucnnr  14960  relexp1g  14961  sgnp  15025  sgnn  15029  absmax  15265  sumss2  15661  fsumsplit  15676  fprodntriv  15877  fprodsplit  15901  ef0lem  16013  rpnnen2lem9  16159  sadadd2  16399  eucalgf  16522  eucalginv  16523  eucalglt  16524  iserodd  16775  pcmpt  16832  pcmpt2  16833  ramtub  16952  prmo1  16977  fvprif  17494  gsumval2a  18622  mgm2nsgrplem2  18856  mgm2nsgrplem3  18857  sgrp2nmndlem3  18862  mulgnn  19017  mulgnegnn  19026  symgextfv  19359  pmtrprfv3  19395  pmtrdifellem4  19420  pmtrprfval  19428  pmtrprfvalrn  19429  odlem2  19480  dfod2  19505  gsumval3a  19844  gsumzsplit  19868  dmdprdsplitlem  19980  ablsimpgfind  20053  abvtrivd  20777  uvcvv0  21757  uvcff  21758  psrlidm  21929  psrridm  21930  mvrcl  21959  mplmon  22002  mplmonmul  22003  mplcoe1  22004  mplcoe5  22007  evlslem3  22047  coe1tmfv2  22229  cply1coe0  22257  cply1coe0bi  22258  gsummoncoe1  22264  mulmarep1gsum1  22529  1marepvsma1  22539  mdetunilem2  22569  mdetunilem9  22576  maducoeval2  22596  symgmatr01lem  22609  gsummatr01lem3  22613  gsummatr01lem4  22614  gsummatr01  22615  m2cpm  22697  m2cpminvid2lem  22710  pmatcollpw3fi1lem1  22742  mp2pm2mplem4  22765  chfacffsupp  22812  chfacfscmul0  22814  chfacfpmmul0  22818  ptpjpre2  23536  ptopn2  23540  xkopt  23611  tsmssplit  24108  xrsxmet  24766  htpycc  24947  pco1  24983  pcohtpylem  24987  pcoass  24992  pcorevlem  24994  ovolunlem1a  25465  ovolunlem1  25466  ovolicc1  25485  itg11  25660  mbfi1flim  25692  itg2split  25718  itg2cnlem1  25730  itgeq2  25747  iblss  25774  itgss2  25782  itgss3  25784  itgless  25786  ibladdlem  25789  itgaddlem1  25792  itggt0  25813  itgcn  25814  dvexp2  25926  lhop2  25988  deg1add  26076  ig1pval3  26151  ply1termlem  26176  plyeq0lem  26183  plypf1  26185  dvply1  26259  pserdvlem2  26406  abelthlem9  26418  logtayllem  26636  logtayl  26637  cxpef  26642  rlimcnp2  26944  efrlim  26947  efrlimOLD  26948  muinv  27171  bposlem5  27267  lgsval2lem  27286  lgsval4  27296  lgsval4a  27298  lgsneg  27300  lgsneg1  27301  lgsdilem  27303  lgsdir  27311  lgsne0  27314  gausslemma2dlem1a  27344  gausslemma2dlem3  27347  2lgslem3  27383  2sqnn0  27417  rplogsumlem2  27464  dchrisum0fno1  27490  rplogsum  27506  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  padicabv  27609  ostth1  27612  ostth3  27617  expnnsval  28434  axlowdim  29046  vtxval  29085  iedgval  29086  funvtxdmge2val  29096  funiedgdmge2val  29097  funvtxdm2val  29098  funiedgdm2val  29099  snstrvtxval  29122  snstriedgval  29123  crctcshwlkn0lem3  29897  crctcsh  29909  clwlkclwwlklem2fv2  30083  eucrct2eupth  30332  fmptunsnop  32789  ind0  32947  ccatws1f1o  33043  pmtridfv1  33188  pmtridfv2  33189  psgnfzto1stlem  33193  elrgspnlem2  33336  elrgspnlem3  33337  elrgspnlem4  33338  elrspunsn  33521  gsummoncoe1fzo  33689  mplmulmvr  33715  evlextv  33718  psrmonmul  33726  esplyfval3  33748  esplyfval1  33749  esplyind  33751  extdgfialglem2  33870  rtelextdg2lem  33903  2sqr3minply  33957  cos9thpiminply  33965  smattr  33976  smatbl  33977  smatbr  33978  1smat1  33981  submatminr1  33987  madjusmdetlem1  34004  madjusmdetlem2  34005  xrge0iifcv  34111  xrge0iif1  34115  esumpinfval  34250  sigaclfu2  34298  eulerpartlemgs2  34557  ballotlemrv2  34699  signswmnd  34734  signswlid  34736  signsvtp  34760  signlem0  34764  ex-sategoelelomsuc  35639  ex-sategoelel12  35640  mrsubcn  35732  bcneg1  35949  bccolsum  35952  dfrdg2  36006  dfrdg4  36164  unblimceq0lem  36725  unbdqndv2lem2  36729  finxpreclem3  37645  finxpreclem5  37647  poimirlem1  37869  poimirlem2  37870  poimirlem7  37875  poimirlem10  37878  poimirlem11  37879  poimirlem16  37884  poimirlem17  37885  poimirlem20  37888  poimirlem24  37892  mblfinlem2  37906  itg2addnclem2  37920  ibladdnclem  37924  ftc1anclem6  37946  ftc1anclem8  37948  fdc  37993  heiborlem6  38064  cdleme31fv2  40766  cdlemefr27cl  40776  sticksstones10  42522  sticksstones12a  42524  sticksstones12  42525  evlsbagval  42924  selvvvval  42940  fsuppssind  42948  mhpind  42949  prjspner1  42981  kelac1  43417  flcidc  43524  oe0suclim  43631  oe0rif  43639  cantnfub  43675  cantnfresb  43678  tfsconcatfv  43695  sqrtcval  43994  relexp01min  44066  relexpxpmin  44070  clsk1indlem0  44394  refsum2cnlem1  45394  upbdrech2  45667  ssfiunibd  45668  ioondisj2  45850  limsup10exlem  46127  icccncfext  46242  cncfiooicclem1  46248  cncfioobdlem  46251  dvnxpaek  46297  dvnprodlem1  46301  ditgeqiooicc  46315  iblcncfioo  46333  volioore  46345  dirkercncflem2  46459  dirkercncflem4  46461  fourierdlem40  46502  fourierdlem56  46517  fourierdlem65  46526  fourierdlem66  46527  fourierdlem73  46534  fourierdlem74  46535  fourierdlem75  46536  fourierdlem78  46539  fourierdlem79  46540  fourierdlem81  46542  fourierdlem82  46543  fourierdlem97  46558  fourierdlem103  46564  fourierdlem104  46565  sqwvfoura  46583  sqwvfourb  46584  fourierswlem  46585  fouriersw  46586  etransclem4  46593  etransclem14  46603  etransclem20  46609  etransclem22  46611  etransclem24  46613  etransclem25  46614  etransclem31  46620  etransclem32  46621  etransclem35  46624  sge0reval  46727  sge0sn  46734  nnfoctbdjlem  46810  isomenndlem  46885  ovnn0val  46906  ovnsubaddlem1  46925  hoidmvn0val  46939  hsphoidmvle2  46940  hsphoidmvle  46941  hoidmvval0  46942  hoidmv1lelem2  46947  hoidmvlelem2  46951  hoidmvlelem3  46952  ovnhoilem1  46956  hspmbllem1  46981  hspmbllem2  46982  volico2  46996  ovolval2lem  46998  ovnsubadd2lem  47000  ovolval4lem1  47004  ovnovollem3  47013  vonioo  47037  vonicc  47040  prproropf1olem3  47862  fdmdifeqresdif  48699  dig1  48965  dignn0flhalflem1  48972  itcoval1  49020  itcoval2  49021  itcoval3  49022  itcovalsuc  49024  ackvalsuc1mpt  49035