Theorem iffalsed 4467

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-if 4457

This theorem is referenced by:  ifeqor  4507  ifnot  4508  ifan  4509  somincom  6028  partfun  6564  mpodifsnif  7367  tz7.44-2  8209  tz7.44-3  8210  unxpdomlem2  8957  sniffsupp  9089  unwdomg  9273  cantnfp1lem1  9366  cantnfp1lem3  9368  cantnflem1d  9376  updjudhcoinrg  9622  ttukeylem7  10202  canthp1lem2  10340  pwfseqlem3  10347  xmulneg1  12932  rexmul  12934  xmulpnf1  12937  fzprval  13246  expnnval  13713  expneg  13718  ccatval2  14211  ccatalpha  14226  swrdnd  14295  swrdnd2  14296  swrd0  14299  swrdccatin2  14370  relexpsucnnr  14664  relexp1g  14665  sgnp  14729  sgnn  14733  absmax  14969  sumss2  15366  fsumsplit  15381  fprodntriv  15580  fprodsplit  15604  ef0lem  15716  rpnnen2lem9  15859  sadadd2  16095  eucalgf  16216  eucalginv  16217  eucalglt  16218  iserodd  16464  pcmpt  16521  pcmpt2  16522  ramtub  16641  prmo1  16666  fvprif  17189  gsumval2a  18284  mgm2nsgrplem2  18473  mgm2nsgrplem3  18474  sgrp2nmndlem3  18479  mulgnn  18623  mulgnegnn  18629  symgextfv  18941  pmtrprfv3  18977  pmtrdifellem4  19002  pmtrprfval  19010  pmtrprfvalrn  19011  odlem2  19062  dfod2  19086  gsumval3a  19419  gsumzsplit  19443  dmdprdsplitlem  19555  ablsimpgfind  19628  abvtrivd  20015  uvcvv0  20907  uvcff  20908  psrlidm  21082  psrridm  21083  mvrcl  21131  mplmon  21146  mplmonmul  21147  mplcoe1  21148  mplcoe5  21151  evlslem3  21200  coe1tmfv2  21356  cply1coe0  21380  cply1coe0bi  21381  gsummoncoe1  21385  mulmarep1gsum1  21630  1marepvsma1  21640  mdetunilem2  21670  mdetunilem9  21677  maducoeval2  21697  symgmatr01lem  21710  gsummatr01lem3  21714  gsummatr01lem4  21715  gsummatr01  21716  m2cpm  21798  m2cpminvid2lem  21811  pmatcollpw3fi1lem1  21843  mp2pm2mplem4  21866  chfacffsupp  21913  chfacfscmul0  21915  chfacfpmmul0  21919  ptpjpre2  22639  ptopn2  22643  xkopt  22714  tsmssplit  23211  xrsxmet  23878  htpycc  24049  pco1  24084  pcohtpylem  24088  pcoass  24093  pcorevlem  24095  ovolunlem1a  24565  ovolunlem1  24566  ovolicc1  24585  itg11  24760  mbfi1flim  24793  itg2split  24819  itg2cnlem1  24831  itgeq2  24847  iblss  24874  itgss2  24882  itgss3  24884  itgless  24886  ibladdlem  24889  itgaddlem1  24892  itggt0  24913  itgcn  24914  dvexp2  25023  lhop2  25084  deg1add  25173  ig1pval3  25244  ply1termlem  25269  plyeq0lem  25276  plypf1  25278  dvply1  25349  pserdvlem2  25492  abelthlem9  25504  logtayllem  25719  logtayl  25720  cxpef  25725  rlimcnp2  26021  efrlim  26024  muinv  26247  bposlem5  26341  lgsval2lem  26360  lgsval4  26370  lgsval4a  26372  lgsneg  26374  lgsneg1  26375  lgsdilem  26377  lgsdir  26385  lgsne0  26388  gausslemma2dlem1a  26418  gausslemma2dlem3  26421  2lgslem3  26457  2sqnn0  26491  rplogsumlem2  26538  dchrisum0fno1  26564  rplogsum  26580  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  padicabv  26683  ostth1  26686  ostth3  26691  axlowdim  27232  vtxval  27273  iedgval  27274  funvtxdmge2val  27284  funiedgdmge2val  27285  funvtxdm2val  27286  funiedgdm2val  27287  snstrvtxval  27310  snstriedgval  27311  crctcshwlkn0lem3  28078  crctcsh  28090  clwlkclwwlklem2fv2  28261  eucrct2eupth  28510  pmtridfv1  31264  pmtridfv2  31265  psgnfzto1stlem  31269  smattr  31651  smatbl  31652  smatbr  31653  1smat1  31656  submatminr1  31662  madjusmdetlem1  31679  madjusmdetlem2  31680  xrge0iifcv  31786  xrge0iif1  31790  ind0  31886  esumpinfval  31941  sigaclfu2  31989  eulerpartlemgs2  32247  ballotlemrv2  32388  signswmnd  32436  signswlid  32438  signsvtp  32462  signlem0  32466  ex-sategoelelomsuc  33288  ex-sategoelel12  33289  mrsubcn  33381  bcneg1  33608  bccolsum  33611  dfrdg2  33677  ttrcltr  33702  dfrdg4  34180  unblimceq0lem  34613  unbdqndv2lem2  34617  finxpreclem3  35491  finxpreclem5  35493  poimirlem1  35705  poimirlem2  35706  poimirlem7  35711  poimirlem10  35714  poimirlem11  35715  poimirlem16  35720  poimirlem17  35721  poimirlem20  35724  poimirlem24  35728  mblfinlem2  35742  itg2addnclem2  35756  ibladdnclem  35760  ftc1anclem6  35782  ftc1anclem8  35784  fdc  35830  heiborlem6  35901  cdleme31fv2  38334  cdlemefr27cl  38344  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  metakunt21  40073  metakunt27  40079  metakunt28  40080  metakunt29  40081  metakunt30  40082  metakunt31  40083  evlsbagval  40198  fsuppssind  40205  mhpind  40206  mhphf  40208  prjspner1  40384  kelac1  40804  flcidc  40915  sqrtcval  41138  relexp01min  41210  relexpxpmin  41214  clsk1indlem0  41540  refsum2cnlem1  42469  upbdrech2  42737  ssfiunibd  42738  ioondisj2  42921  limsup10exlem  43203  icccncfext  43318  cncfiooicclem1  43324  cncfioobdlem  43327  dvnxpaek  43373  dvnprodlem1  43377  ditgeqiooicc  43391  iblcncfioo  43409  volioore  43421  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem40  43578  fourierdlem56  43593  fourierdlem65  43602  fourierdlem66  43603  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem78  43615  fourierdlem79  43616  fourierdlem81  43618  fourierdlem82  43619  fourierdlem97  43634  fourierdlem103  43640  fourierdlem104  43641  sqwvfoura  43659  sqwvfourb  43660  fourierswlem  43661  fouriersw  43662  etransclem4  43669  etransclem14  43679  etransclem20  43685  etransclem22  43687  etransclem24  43689  etransclem25  43690  etransclem31  43696  etransclem32  43697  etransclem35  43700  sge0reval  43800  sge0sn  43807  nnfoctbdjlem  43883  isomenndlem  43958  ovnn0val  43979  ovnsubaddlem1  43998  hoidmvn0val  44012  hsphoidmvle2  44013  hsphoidmvle  44014  hoidmvval0  44015  hoidmv1lelem2  44020  hoidmvlelem2  44024  hoidmvlelem3  44025  ovnhoilem1  44029  hspmbllem1  44054  hspmbllem2  44055  volico2  44069  ovolval2lem  44071  ovnsubadd2lem  44073  ovolval4lem1  44077  ovnovollem3  44086  vonioo  44110  vonicc  44113  prproropf1olem3  44845  fdmdifeqresdif  45565  dig1  45842  dignn0flhalflem1  45849  itcoval1  45897  itcoval2  45898  itcoval3  45899  itcovalsuc  45901  ackvalsuc1mpt  45912