Theorem iffalsed 4471

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

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

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-if 4461

This theorem is referenced by:  ifeqor  4511  ifnot  4512  ifan  4513  somincom  6044  partfun  6589  mpodifsnif  7398  tz7.44-2  8247  tz7.44-3  8248  unxpdomlem2  9037  sniffsupp  9168  unwdomg  9352  cantnfp1lem1  9445  cantnfp1lem3  9447  cantnflem1d  9455  ttrcltr  9483  updjudhcoinrg  9700  ttukeylem7  10280  canthp1lem2  10418  pwfseqlem3  10425  xmulneg1  13012  rexmul  13014  xmulpnf1  13017  fzprval  13326  expnnval  13794  expneg  13799  ccatval2  14292  ccatalpha  14307  swrdnd  14376  swrdnd2  14377  swrd0  14380  swrdccatin2  14451  relexpsucnnr  14745  relexp1g  14746  sgnp  14810  sgnn  14814  absmax  15050  sumss2  15447  fsumsplit  15462  fprodntriv  15661  fprodsplit  15685  ef0lem  15797  rpnnen2lem9  15940  sadadd2  16176  eucalgf  16297  eucalginv  16298  eucalglt  16299  iserodd  16545  pcmpt  16602  pcmpt2  16603  ramtub  16722  prmo1  16747  fvprif  17281  gsumval2a  18378  mgm2nsgrplem2  18567  mgm2nsgrplem3  18568  sgrp2nmndlem3  18573  mulgnn  18717  mulgnegnn  18723  symgextfv  19035  pmtrprfv3  19071  pmtrdifellem4  19096  pmtrprfval  19104  pmtrprfvalrn  19105  odlem2  19156  dfod2  19180  gsumval3a  19513  gsumzsplit  19537  dmdprdsplitlem  19649  ablsimpgfind  19722  abvtrivd  20109  uvcvv0  21006  uvcff  21007  psrlidm  21181  psrridm  21182  mvrcl  21230  mplmon  21245  mplmonmul  21246  mplcoe1  21247  mplcoe5  21250  evlslem3  21299  coe1tmfv2  21455  cply1coe0  21479  cply1coe0bi  21480  gsummoncoe1  21484  mulmarep1gsum1  21731  1marepvsma1  21741  mdetunilem2  21771  mdetunilem9  21778  maducoeval2  21798  symgmatr01lem  21811  gsummatr01lem3  21815  gsummatr01lem4  21816  gsummatr01  21817  m2cpm  21899  m2cpminvid2lem  21912  pmatcollpw3fi1lem1  21944  mp2pm2mplem4  21967  chfacffsupp  22014  chfacfscmul0  22016  chfacfpmmul0  22020  ptpjpre2  22740  ptopn2  22744  xkopt  22815  tsmssplit  23312  xrsxmet  23981  htpycc  24152  pco1  24187  pcohtpylem  24191  pcoass  24196  pcorevlem  24198  ovolunlem1a  24669  ovolunlem1  24670  ovolicc1  24689  itg11  24864  mbfi1flim  24897  itg2split  24923  itg2cnlem1  24935  itgeq2  24951  iblss  24978  itgss2  24986  itgss3  24988  itgless  24990  ibladdlem  24993  itgaddlem1  24996  itggt0  25017  itgcn  25018  dvexp2  25127  lhop2  25188  deg1add  25277  ig1pval3  25348  ply1termlem  25373  plyeq0lem  25380  plypf1  25382  dvply1  25453  pserdvlem2  25596  abelthlem9  25608  logtayllem  25823  logtayl  25824  cxpef  25829  rlimcnp2  26125  efrlim  26128  muinv  26351  bposlem5  26445  lgsval2lem  26464  lgsval4  26474  lgsval4a  26476  lgsneg  26478  lgsneg1  26479  lgsdilem  26481  lgsdir  26489  lgsne0  26492  gausslemma2dlem1a  26522  gausslemma2dlem3  26525  2lgslem3  26561  2sqnn0  26595  rplogsumlem2  26642  dchrisum0fno1  26668  rplogsum  26684  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  padicabv  26787  ostth1  26790  ostth3  26795  axlowdim  27338  vtxval  27379  iedgval  27380  funvtxdmge2val  27390  funiedgdmge2val  27391  funvtxdm2val  27392  funiedgdm2val  27393  snstrvtxval  27416  snstriedgval  27417  crctcshwlkn0lem3  28186  crctcsh  28198  clwlkclwwlklem2fv2  28369  eucrct2eupth  28618  pmtridfv1  31371  pmtridfv2  31372  psgnfzto1stlem  31376  smattr  31758  smatbl  31759  smatbr  31760  1smat1  31763  submatminr1  31769  madjusmdetlem1  31786  madjusmdetlem2  31787  xrge0iifcv  31893  xrge0iif1  31897  ind0  31995  esumpinfval  32050  sigaclfu2  32098  eulerpartlemgs2  32356  ballotlemrv2  32497  signswmnd  32545  signswlid  32547  signsvtp  32571  signlem0  32575  ex-sategoelelomsuc  33397  ex-sategoelel12  33398  mrsubcn  33490  bcneg1  33711  bccolsum  33714  dfrdg2  33780  dfrdg4  34262  unblimceq0lem  34695  unbdqndv2lem2  34699  finxpreclem3  35573  finxpreclem5  35575  poimirlem1  35787  poimirlem2  35788  poimirlem7  35793  poimirlem10  35796  poimirlem11  35797  poimirlem16  35802  poimirlem17  35803  poimirlem20  35806  poimirlem24  35810  mblfinlem2  35824  itg2addnclem2  35838  ibladdnclem  35842  ftc1anclem6  35864  ftc1anclem8  35866  fdc  35912  heiborlem6  35983  cdleme31fv2  38414  cdlemefr27cl  38424  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  metakunt21  40152  metakunt27  40158  metakunt28  40159  metakunt29  40160  metakunt30  40161  metakunt31  40162  evlsbagval  40282  fsuppssind  40289  mhpind  40290  mhphf  40292  prjspner1  40470  kelac1  40895  flcidc  41006  sqrtcval  41256  relexp01min  41328  relexpxpmin  41332  clsk1indlem0  41658  refsum2cnlem1  42587  upbdrech2  42854  ssfiunibd  42855  ioondisj2  43038  limsup10exlem  43320  icccncfext  43435  cncfiooicclem1  43441  cncfioobdlem  43444  dvnxpaek  43490  dvnprodlem1  43494  ditgeqiooicc  43508  iblcncfioo  43526  volioore  43538  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem40  43695  fourierdlem56  43710  fourierdlem65  43719  fourierdlem66  43720  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem78  43732  fourierdlem79  43733  fourierdlem81  43735  fourierdlem82  43736  fourierdlem97  43751  fourierdlem103  43757  fourierdlem104  43758  sqwvfoura  43776  sqwvfourb  43777  fourierswlem  43778  fouriersw  43779  etransclem4  43786  etransclem14  43796  etransclem20  43802  etransclem22  43804  etransclem24  43806  etransclem25  43807  etransclem31  43813  etransclem32  43814  etransclem35  43817  sge0reval  43917  sge0sn  43924  nnfoctbdjlem  44000  isomenndlem  44075  ovnn0val  44096  ovnsubaddlem1  44115  hoidmvn0val  44129  hsphoidmvle2  44130  hsphoidmvle  44131  hoidmvval0  44132  hoidmv1lelem2  44137  hoidmvlelem2  44141  hoidmvlelem3  44142  ovnhoilem1  44146  hspmbllem1  44171  hspmbllem2  44172  volico2  44186  ovolval2lem  44188  ovnsubadd2lem  44190  ovolval4lem1  44194  ovnovollem3  44203  vonioo  44227  vonicc  44230  prproropf1olem3  44968  fdmdifeqresdif  45688  dig1  45965  dignn0flhalflem1  45972  itcoval1  46020  itcoval2  46021  itcoval3  46022  itcovalsuc  46024  ackvalsuc1mpt  46035