Theorem iffalsed 4450

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1543  ifcif 4439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4440

This theorem is referenced by:  ifeqor  4490  ifnot  4491  ifan  4492  somincom  5999  partfun  6525  mpodifsnif  7325  tz7.44-2  8143  tz7.44-3  8144  unxpdomlem2  8883  sniffsupp  9016  unwdomg  9200  cantnfp1lem1  9293  cantnfp1lem3  9295  cantnflem1d  9303  updjudhcoinrg  9549  ttukeylem7  10129  canthp1lem2  10267  pwfseqlem3  10274  xmulneg1  12859  rexmul  12861  xmulpnf1  12864  fzprval  13173  expnnval  13638  expneg  13643  ccatval2  14135  ccatalpha  14150  swrdnd  14219  swrdnd2  14220  swrd0  14223  swrdccatin2  14294  relexpsucnnr  14588  relexp1g  14589  sgnp  14653  sgnn  14657  absmax  14893  sumss2  15290  fsumsplit  15305  fprodntriv  15504  fprodsplit  15528  ef0lem  15640  rpnnen2lem9  15783  sadadd2  16019  eucalgf  16140  eucalginv  16141  eucalglt  16142  iserodd  16388  pcmpt  16445  pcmpt2  16446  ramtub  16565  prmo1  16590  fvprif  17066  gsumval2a  18157  mgm2nsgrplem2  18346  mgm2nsgrplem3  18347  sgrp2nmndlem3  18352  mulgnn  18496  mulgnegnn  18502  symgextfv  18810  pmtrprfv3  18846  pmtrdifellem4  18871  pmtrprfval  18879  pmtrprfvalrn  18880  odlem2  18931  dfod2  18955  gsumval3a  19288  gsumzsplit  19312  dmdprdsplitlem  19424  ablsimpgfind  19497  abvtrivd  19876  uvcvv0  20752  uvcff  20753  psrlidm  20928  psrridm  20929  mvrcl  20977  mplmon  20992  mplmonmul  20993  mplcoe1  20994  mplcoe5  20997  evlslem3  21040  coe1tmfv2  21196  cply1coe0  21220  cply1coe0bi  21221  gsummoncoe1  21225  mulmarep1gsum1  21470  1marepvsma1  21480  mdetunilem2  21510  mdetunilem9  21517  maducoeval2  21537  symgmatr01lem  21550  gsummatr01lem3  21554  gsummatr01lem4  21555  gsummatr01  21556  m2cpm  21638  m2cpminvid2lem  21651  pmatcollpw3fi1lem1  21683  mp2pm2mplem4  21706  chfacffsupp  21753  chfacfscmul0  21755  chfacfpmmul0  21759  ptpjpre2  22477  ptopn2  22481  xkopt  22552  tsmssplit  23049  xrsxmet  23706  htpycc  23877  pco1  23912  pcohtpylem  23916  pcoass  23921  pcorevlem  23923  ovolunlem1a  24393  ovolunlem1  24394  ovolicc1  24413  itg11  24588  mbfi1flim  24621  itg2split  24647  itg2cnlem1  24659  itgeq2  24675  iblss  24702  itgss2  24710  itgss3  24712  itgless  24714  ibladdlem  24717  itgaddlem1  24720  itggt0  24741  itgcn  24742  dvexp2  24851  lhop2  24912  deg1add  25001  ig1pval3  25072  ply1termlem  25097  plyeq0lem  25104  plypf1  25106  dvply1  25177  pserdvlem2  25320  abelthlem9  25332  logtayllem  25547  logtayl  25548  cxpef  25553  rlimcnp2  25849  efrlim  25852  muinv  26075  bposlem5  26169  lgsval2lem  26188  lgsval4  26198  lgsval4a  26200  lgsneg  26202  lgsneg1  26203  lgsdilem  26205  lgsdir  26213  lgsne0  26216  gausslemma2dlem1a  26246  gausslemma2dlem3  26249  2lgslem3  26285  2sqnn0  26319  rplogsumlem2  26366  dchrisum0fno1  26392  rplogsum  26408  pntrlog2bndlem4  26461  pntrlog2bndlem5  26462  padicabv  26511  ostth1  26514  ostth3  26519  axlowdim  27052  vtxval  27091  iedgval  27092  funvtxdmge2val  27102  funiedgdmge2val  27103  funvtxdm2val  27104  funiedgdm2val  27105  snstrvtxval  27128  snstriedgval  27129  crctcshwlkn0lem3  27896  crctcsh  27908  clwlkclwwlklem2fv2  28079  eucrct2eupth  28328  pmtridfv1  31081  pmtridfv2  31082  psgnfzto1stlem  31086  smattr  31463  smatbl  31464  smatbr  31465  1smat1  31468  submatminr1  31474  madjusmdetlem1  31491  madjusmdetlem2  31492  xrge0iifcv  31598  xrge0iif1  31602  ind0  31698  esumpinfval  31753  sigaclfu2  31801  eulerpartlemgs2  32059  ballotlemrv2  32200  signswmnd  32248  signswlid  32250  signsvtp  32274  signlem0  32278  ex-sategoelelomsuc  33101  ex-sategoelel12  33102  mrsubcn  33194  bcneg1  33420  bccolsum  33423  dfrdg2  33490  ttrcltr  33515  dfrdg4  33990  unblimceq0lem  34423  unbdqndv2lem2  34427  finxpreclem3  35301  finxpreclem5  35303  poimirlem1  35515  poimirlem2  35516  poimirlem7  35521  poimirlem10  35524  poimirlem11  35525  poimirlem16  35530  poimirlem17  35531  poimirlem20  35534  poimirlem24  35538  mblfinlem2  35552  itg2addnclem2  35566  ibladdnclem  35570  ftc1anclem6  35592  ftc1anclem8  35594  fdc  35640  heiborlem6  35711  cdleme31fv2  38144  cdlemefr27cl  38154  sticksstones10  39833  sticksstones12a  39835  sticksstones12  39836  metakunt21  39867  metakunt27  39873  metakunt28  39874  metakunt29  39875  metakunt30  39876  metakunt31  39877  evlsbagval  39985  fsuppssind  39992  mhpind  39993  mhphf  39995  prjspner1  40171  kelac1  40591  flcidc  40702  sqrtcval  40925  relexp01min  40998  relexpxpmin  41002  clsk1indlem0  41328  refsum2cnlem1  42253  upbdrech2  42520  ssfiunibd  42521  ioondisj2  42706  limsup10exlem  42988  icccncfext  43103  cncfiooicclem1  43109  cncfioobdlem  43112  dvnxpaek  43158  dvnprodlem1  43162  ditgeqiooicc  43176  iblcncfioo  43194  volioore  43206  dirkercncflem2  43320  dirkercncflem4  43322  fourierdlem40  43363  fourierdlem56  43378  fourierdlem65  43387  fourierdlem66  43388  fourierdlem73  43395  fourierdlem74  43396  fourierdlem75  43397  fourierdlem78  43400  fourierdlem79  43401  fourierdlem81  43403  fourierdlem82  43404  fourierdlem97  43419  fourierdlem103  43425  fourierdlem104  43426  sqwvfoura  43444  sqwvfourb  43445  fourierswlem  43446  fouriersw  43447  etransclem4  43454  etransclem14  43464  etransclem20  43470  etransclem22  43472  etransclem24  43474  etransclem25  43475  etransclem31  43481  etransclem32  43482  etransclem35  43485  sge0reval  43585  sge0sn  43592  nnfoctbdjlem  43668  isomenndlem  43743  ovnn0val  43764  ovnsubaddlem1  43783  hoidmvn0val  43797  hsphoidmvle2  43798  hsphoidmvle  43799  hoidmvval0  43800  hoidmv1lelem2  43805  hoidmvlelem2  43809  hoidmvlelem3  43810  ovnhoilem1  43814  hspmbllem1  43839  hspmbllem2  43840  volico2  43854  ovolval2lem  43856  ovnsubadd2lem  43858  ovolval4lem1  43862  ovnovollem3  43871  vonioo  43895  vonicc  43898  prproropf1olem3  44630  fdmdifeqresdif  45350  dig1  45627  dignn0flhalflem1  45634  itcoval1  45682  itcoval2  45683  itcoval3  45684  itcovalsuc  45686  ackvalsuc1mpt  45697