Theorem iffalsed 4538

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-if 4528

This theorem is referenced by:  ifeqor  4578  ifnot  4579  ifan  4580  somincom  6134  partfun  6696  mpodifsnif  7525  tz7.44-2  8409  tz7.44-3  8410  unxpdomlem2  9253  sniffsupp  9397  unwdomg  9581  cantnfp1lem1  9675  cantnfp1lem3  9677  cantnflem1d  9685  ttrcltr  9713  updjudhcoinrg  9930  ttukeylem7  10512  canthp1lem2  10650  pwfseqlem3  10657  xmulneg1  13252  rexmul  13254  xmulpnf1  13257  fzprval  13566  expnnval  14034  expneg  14039  ccatval2  14532  ccatalpha  14547  swrdnd  14608  swrdnd2  14609  swrd0  14612  swrdccatin2  14683  relexpsucnnr  14976  relexp1g  14977  sgnp  15041  sgnn  15045  absmax  15280  sumss2  15676  fsumsplit  15691  fprodntriv  15890  fprodsplit  15914  ef0lem  16026  rpnnen2lem9  16169  sadadd2  16405  eucalgf  16524  eucalginv  16525  eucalglt  16526  iserodd  16772  pcmpt  16829  pcmpt2  16830  ramtub  16949  prmo1  16974  fvprif  17511  gsumval2a  18610  mgm2nsgrplem2  18836  mgm2nsgrplem3  18837  sgrp2nmndlem3  18842  mulgnn  18994  mulgnegnn  19000  symgextfv  19327  pmtrprfv3  19363  pmtrdifellem4  19388  pmtrprfval  19396  pmtrprfvalrn  19397  odlem2  19448  dfod2  19473  gsumval3a  19812  gsumzsplit  19836  dmdprdsplitlem  19948  ablsimpgfind  20021  abvtrivd  20591  uvcvv0  21564  uvcff  21565  psrlidm  21742  psrridm  21743  mvrcl  21770  mplmon  21809  mplmonmul  21810  mplcoe1  21811  mplcoe5  21814  evlslem3  21862  coe1tmfv2  22017  cply1coe0  22043  cply1coe0bi  22044  gsummoncoe1  22048  mulmarep1gsum1  22295  1marepvsma1  22305  mdetunilem2  22335  mdetunilem9  22342  maducoeval2  22362  symgmatr01lem  22375  gsummatr01lem3  22379  gsummatr01lem4  22380  gsummatr01  22381  m2cpm  22463  m2cpminvid2lem  22476  pmatcollpw3fi1lem1  22508  mp2pm2mplem4  22531  chfacffsupp  22578  chfacfscmul0  22580  chfacfpmmul0  22584  ptpjpre2  23304  ptopn2  23308  xkopt  23379  tsmssplit  23876  xrsxmet  24545  htpycc  24726  pco1  24762  pcohtpylem  24766  pcoass  24771  pcorevlem  24773  ovolunlem1a  25245  ovolunlem1  25246  ovolicc1  25265  itg11  25440  mbfi1flim  25473  itg2split  25499  itg2cnlem1  25511  itgeq2  25527  iblss  25554  itgss2  25562  itgss3  25564  itgless  25566  ibladdlem  25569  itgaddlem1  25572  itggt0  25593  itgcn  25594  dvexp2  25706  lhop2  25767  deg1add  25856  ig1pval3  25927  ply1termlem  25952  plyeq0lem  25959  plypf1  25961  dvply1  26033  pserdvlem2  26176  abelthlem9  26188  logtayllem  26403  logtayl  26404  cxpef  26409  rlimcnp2  26707  efrlim  26710  muinv  26933  bposlem5  27027  lgsval2lem  27046  lgsval4  27056  lgsval4a  27058  lgsneg  27060  lgsneg1  27061  lgsdilem  27063  lgsdir  27071  lgsne0  27074  gausslemma2dlem1a  27104  gausslemma2dlem3  27107  2lgslem3  27143  2sqnn0  27177  rplogsumlem2  27224  dchrisum0fno1  27250  rplogsum  27266  pntrlog2bndlem4  27319  pntrlog2bndlem5  27320  padicabv  27369  ostth1  27372  ostth3  27377  axlowdim  28486  vtxval  28527  iedgval  28528  funvtxdmge2val  28538  funiedgdmge2val  28539  funvtxdm2val  28540  funiedgdm2val  28541  snstrvtxval  28564  snstriedgval  28565  crctcshwlkn0lem3  29333  crctcsh  29345  clwlkclwwlklem2fv2  29516  eucrct2eupth  29765  pmtridfv1  32524  pmtridfv2  32525  psgnfzto1stlem  32529  elrspunsn  32821  gsummoncoe1fzo  32943  smattr  33077  smatbl  33078  smatbr  33079  1smat1  33082  submatminr1  33088  madjusmdetlem1  33105  madjusmdetlem2  33106  xrge0iifcv  33212  xrge0iif1  33216  ind0  33314  esumpinfval  33369  sigaclfu2  33417  eulerpartlemgs2  33677  ballotlemrv2  33818  signswmnd  33866  signswlid  33868  signsvtp  33892  signlem0  33896  ex-sategoelelomsuc  34715  ex-sategoelel12  34716  mrsubcn  34808  bcneg1  35010  bccolsum  35013  dfrdg2  35071  dfrdg4  35227  unblimceq0lem  35685  unbdqndv2lem2  35689  finxpreclem3  36577  finxpreclem5  36579  poimirlem1  36792  poimirlem2  36793  poimirlem7  36798  poimirlem10  36801  poimirlem11  36802  poimirlem16  36807  poimirlem17  36808  poimirlem20  36811  poimirlem24  36815  mblfinlem2  36829  itg2addnclem2  36843  ibladdnclem  36847  ftc1anclem6  36869  ftc1anclem8  36871  fdc  36916  heiborlem6  36987  cdleme31fv2  39567  cdlemefr27cl  39577  sticksstones10  41277  sticksstones12a  41279  sticksstones12  41280  metakunt21  41311  metakunt27  41317  metakunt28  41318  metakunt29  41319  metakunt30  41320  metakunt31  41321  evlsbagval  41440  selvvvval  41459  fsuppssind  41467  mhpind  41468  prjspner1  41670  kelac1  42107  flcidc  42218  oe0suclim  42329  oe0rif  42337  cantnfub  42373  cantnfresb  42376  tfsconcatfv  42393  sqrtcval  42694  relexp01min  42766  relexpxpmin  42770  clsk1indlem0  43094  refsum2cnlem1  44023  upbdrech2  44316  ssfiunibd  44317  ioondisj2  44504  limsup10exlem  44786  icccncfext  44901  cncfiooicclem1  44907  cncfioobdlem  44910  dvnxpaek  44956  dvnprodlem1  44960  ditgeqiooicc  44974  iblcncfioo  44992  volioore  45004  dirkercncflem2  45118  dirkercncflem4  45120  fourierdlem40  45161  fourierdlem56  45176  fourierdlem65  45185  fourierdlem66  45186  fourierdlem73  45193  fourierdlem74  45194  fourierdlem75  45195  fourierdlem78  45198  fourierdlem79  45199  fourierdlem81  45201  fourierdlem82  45202  fourierdlem97  45217  fourierdlem103  45223  fourierdlem104  45224  sqwvfoura  45242  sqwvfourb  45243  fourierswlem  45244  fouriersw  45245  etransclem4  45252  etransclem14  45262  etransclem20  45268  etransclem22  45270  etransclem24  45272  etransclem25  45273  etransclem31  45279  etransclem32  45280  etransclem35  45283  sge0reval  45386  sge0sn  45393  nnfoctbdjlem  45469  isomenndlem  45544  ovnn0val  45565  ovnsubaddlem1  45584  hoidmvn0val  45598  hsphoidmvle2  45599  hsphoidmvle  45600  hoidmvval0  45601  hoidmv1lelem2  45606  hoidmvlelem2  45610  hoidmvlelem3  45611  ovnhoilem1  45615  hspmbllem1  45640  hspmbllem2  45641  volico2  45655  ovolval2lem  45657  ovnsubadd2lem  45659  ovolval4lem1  45663  ovnovollem3  45672  vonioo  45696  vonicc  45699  prproropf1olem3  46471  fdmdifeqresdif  47105  dig1  47381  dignn0flhalflem1  47388  itcoval1  47436  itcoval2  47437  itcoval3  47438  itcovalsuc  47440  ackvalsuc1mpt  47451