Theorem iffalsed 4539

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4529

This theorem is referenced by:  ifeqor  4579  ifnot  4580  ifan  4581  somincom  6133  partfun  6695  mpodifsnif  7520  tz7.44-2  8404  tz7.44-3  8405  unxpdomlem2  9248  sniffsupp  9392  unwdomg  9576  cantnfp1lem1  9670  cantnfp1lem3  9672  cantnflem1d  9680  ttrcltr  9708  updjudhcoinrg  9925  ttukeylem7  10507  canthp1lem2  10645  pwfseqlem3  10652  xmulneg1  13245  rexmul  13247  xmulpnf1  13250  fzprval  13559  expnnval  14027  expneg  14032  ccatval2  14525  ccatalpha  14540  swrdnd  14601  swrdnd2  14602  swrd0  14605  swrdccatin2  14676  relexpsucnnr  14969  relexp1g  14970  sgnp  15034  sgnn  15038  absmax  15273  sumss2  15669  fsumsplit  15684  fprodntriv  15883  fprodsplit  15907  ef0lem  16019  rpnnen2lem9  16162  sadadd2  16398  eucalgf  16517  eucalginv  16518  eucalglt  16519  iserodd  16765  pcmpt  16822  pcmpt2  16823  ramtub  16942  prmo1  16967  fvprif  17504  gsumval2a  18601  mgm2nsgrplem2  18797  mgm2nsgrplem3  18798  sgrp2nmndlem3  18803  mulgnn  18953  mulgnegnn  18959  symgextfv  19281  pmtrprfv3  19317  pmtrdifellem4  19342  pmtrprfval  19350  pmtrprfvalrn  19351  odlem2  19402  dfod2  19427  gsumval3a  19766  gsumzsplit  19790  dmdprdsplitlem  19902  ablsimpgfind  19975  abvtrivd  20441  uvcvv0  21337  uvcff  21338  psrlidm  21515  psrridm  21516  mvrcl  21543  mplmon  21582  mplmonmul  21583  mplcoe1  21584  mplcoe5  21587  evlslem3  21635  coe1tmfv2  21789  cply1coe0  21815  cply1coe0bi  21816  gsummoncoe1  21820  mulmarep1gsum1  22067  1marepvsma1  22077  mdetunilem2  22107  mdetunilem9  22114  maducoeval2  22134  symgmatr01lem  22147  gsummatr01lem3  22151  gsummatr01lem4  22152  gsummatr01  22153  m2cpm  22235  m2cpminvid2lem  22248  pmatcollpw3fi1lem1  22280  mp2pm2mplem4  22303  chfacffsupp  22350  chfacfscmul0  22352  chfacfpmmul0  22356  ptpjpre2  23076  ptopn2  23080  xkopt  23151  tsmssplit  23648  xrsxmet  24317  htpycc  24488  pco1  24523  pcohtpylem  24527  pcoass  24532  pcorevlem  24534  ovolunlem1a  25005  ovolunlem1  25006  ovolicc1  25025  itg11  25200  mbfi1flim  25233  itg2split  25259  itg2cnlem1  25271  itgeq2  25287  iblss  25314  itgss2  25322  itgss3  25324  itgless  25326  ibladdlem  25329  itgaddlem1  25332  itggt0  25353  itgcn  25354  dvexp2  25463  lhop2  25524  deg1add  25613  ig1pval3  25684  ply1termlem  25709  plyeq0lem  25716  plypf1  25718  dvply1  25789  pserdvlem2  25932  abelthlem9  25944  logtayllem  26159  logtayl  26160  cxpef  26165  rlimcnp2  26461  efrlim  26464  muinv  26687  bposlem5  26781  lgsval2lem  26800  lgsval4  26810  lgsval4a  26812  lgsneg  26814  lgsneg1  26815  lgsdilem  26817  lgsdir  26825  lgsne0  26828  gausslemma2dlem1a  26858  gausslemma2dlem3  26861  2lgslem3  26897  2sqnn0  26931  rplogsumlem2  26978  dchrisum0fno1  27004  rplogsum  27020  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  padicabv  27123  ostth1  27126  ostth3  27131  axlowdim  28209  vtxval  28250  iedgval  28251  funvtxdmge2val  28261  funiedgdmge2val  28262  funvtxdm2val  28263  funiedgdm2val  28264  snstrvtxval  28287  snstriedgval  28288  crctcshwlkn0lem3  29056  crctcsh  29068  clwlkclwwlklem2fv2  29239  eucrct2eupth  29488  pmtridfv1  32242  pmtridfv2  32243  psgnfzto1stlem  32247  elrspunsn  32536  gsummoncoe1fzo  32657  smattr  32768  smatbl  32769  smatbr  32770  1smat1  32773  submatminr1  32779  madjusmdetlem1  32796  madjusmdetlem2  32797  xrge0iifcv  32903  xrge0iif1  32907  ind0  33005  esumpinfval  33060  sigaclfu2  33108  eulerpartlemgs2  33368  ballotlemrv2  33509  signswmnd  33557  signswlid  33559  signsvtp  33583  signlem0  33587  ex-sategoelelomsuc  34406  ex-sategoelel12  34407  mrsubcn  34499  bcneg1  34695  bccolsum  34698  dfrdg2  34756  dfrdg4  34912  unblimceq0lem  35371  unbdqndv2lem2  35375  finxpreclem3  36263  finxpreclem5  36265  poimirlem1  36478  poimirlem2  36479  poimirlem7  36484  poimirlem10  36487  poimirlem11  36488  poimirlem16  36493  poimirlem17  36494  poimirlem20  36497  poimirlem24  36501  mblfinlem2  36515  itg2addnclem2  36529  ibladdnclem  36533  ftc1anclem6  36555  ftc1anclem8  36557  fdc  36602  heiborlem6  36673  cdleme31fv2  39253  cdlemefr27cl  39263  sticksstones10  40960  sticksstones12a  40962  sticksstones12  40963  metakunt21  40994  metakunt27  41000  metakunt28  41001  metakunt29  41002  metakunt30  41003  metakunt31  41004  evlsbagval  41136  selvvvval  41155  fsuppssind  41163  mhpind  41164  prjspner1  41365  kelac1  41791  flcidc  41902  oe0suclim  42013  oe0rif  42021  cantnfub  42057  cantnfresb  42060  tfsconcatfv  42077  sqrtcval  42378  relexp01min  42450  relexpxpmin  42454  clsk1indlem0  42778  refsum2cnlem1  43707  upbdrech2  44005  ssfiunibd  44006  ioondisj2  44193  limsup10exlem  44475  icccncfext  44590  cncfiooicclem1  44596  cncfioobdlem  44599  dvnxpaek  44645  dvnprodlem1  44649  ditgeqiooicc  44663  iblcncfioo  44681  volioore  44693  dirkercncflem2  44807  dirkercncflem4  44809  fourierdlem40  44850  fourierdlem56  44865  fourierdlem65  44874  fourierdlem66  44875  fourierdlem73  44882  fourierdlem74  44883  fourierdlem75  44884  fourierdlem78  44887  fourierdlem79  44888  fourierdlem81  44890  fourierdlem82  44891  fourierdlem97  44906  fourierdlem103  44912  fourierdlem104  44913  sqwvfoura  44931  sqwvfourb  44932  fourierswlem  44933  fouriersw  44934  etransclem4  44941  etransclem14  44951  etransclem20  44957  etransclem22  44959  etransclem24  44961  etransclem25  44962  etransclem31  44968  etransclem32  44969  etransclem35  44972  sge0reval  45075  sge0sn  45082  nnfoctbdjlem  45158  isomenndlem  45233  ovnn0val  45254  ovnsubaddlem1  45273  hoidmvn0val  45287  hsphoidmvle2  45288  hsphoidmvle  45289  hoidmvval0  45290  hoidmv1lelem2  45295  hoidmvlelem2  45299  hoidmvlelem3  45300  ovnhoilem1  45304  hspmbllem1  45329  hspmbllem2  45330  volico2  45344  ovolval2lem  45346  ovnsubadd2lem  45348  ovolval4lem1  45352  ovnovollem3  45361  vonioo  45385  vonicc  45388  prproropf1olem3  46160  fdmdifeqresdif  46971  dig1  47248  dignn0flhalflem1  47255  itcoval1  47303  itcoval2  47304  itcoval3  47305  itcovalsuc  47307  ackvalsuc1mpt  47318