Theorem iffalsed 4540

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

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

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 4530

This theorem is referenced by:  ifeqor  4580  ifnot  4581  ifan  4582  somincom  6136  partfun  6698  mpodifsnif  7523  tz7.44-2  8407  tz7.44-3  8408  unxpdomlem2  9251  sniffsupp  9395  unwdomg  9579  cantnfp1lem1  9673  cantnfp1lem3  9675  cantnflem1d  9683  ttrcltr  9711  updjudhcoinrg  9928  ttukeylem7  10510  canthp1lem2  10648  pwfseqlem3  10655  xmulneg1  13248  rexmul  13250  xmulpnf1  13253  fzprval  13562  expnnval  14030  expneg  14035  ccatval2  14528  ccatalpha  14543  swrdnd  14604  swrdnd2  14605  swrd0  14608  swrdccatin2  14679  relexpsucnnr  14972  relexp1g  14973  sgnp  15037  sgnn  15041  absmax  15276  sumss2  15672  fsumsplit  15687  fprodntriv  15886  fprodsplit  15910  ef0lem  16022  rpnnen2lem9  16165  sadadd2  16401  eucalgf  16520  eucalginv  16521  eucalglt  16522  iserodd  16768  pcmpt  16825  pcmpt2  16826  ramtub  16945  prmo1  16970  fvprif  17507  gsumval2a  18604  mgm2nsgrplem2  18800  mgm2nsgrplem3  18801  sgrp2nmndlem3  18806  mulgnn  18958  mulgnegnn  18964  symgextfv  19286  pmtrprfv3  19322  pmtrdifellem4  19347  pmtrprfval  19355  pmtrprfvalrn  19356  odlem2  19407  dfod2  19432  gsumval3a  19771  gsumzsplit  19795  dmdprdsplitlem  19907  ablsimpgfind  19980  abvtrivd  20448  uvcvv0  21345  uvcff  21346  psrlidm  21523  psrridm  21524  mvrcl  21551  mplmon  21590  mplmonmul  21591  mplcoe1  21592  mplcoe5  21595  evlslem3  21643  coe1tmfv2  21797  cply1coe0  21823  cply1coe0bi  21824  gsummoncoe1  21828  mulmarep1gsum1  22075  1marepvsma1  22085  mdetunilem2  22115  mdetunilem9  22122  maducoeval2  22142  symgmatr01lem  22155  gsummatr01lem3  22159  gsummatr01lem4  22160  gsummatr01  22161  m2cpm  22243  m2cpminvid2lem  22256  pmatcollpw3fi1lem1  22288  mp2pm2mplem4  22311  chfacffsupp  22358  chfacfscmul0  22360  chfacfpmmul0  22364  ptpjpre2  23084  ptopn2  23088  xkopt  23159  tsmssplit  23656  xrsxmet  24325  htpycc  24496  pco1  24531  pcohtpylem  24535  pcoass  24540  pcorevlem  24542  ovolunlem1a  25013  ovolunlem1  25014  ovolicc1  25033  itg11  25208  mbfi1flim  25241  itg2split  25267  itg2cnlem1  25279  itgeq2  25295  iblss  25322  itgss2  25330  itgss3  25332  itgless  25334  ibladdlem  25337  itgaddlem1  25340  itggt0  25361  itgcn  25362  dvexp2  25471  lhop2  25532  deg1add  25621  ig1pval3  25692  ply1termlem  25717  plyeq0lem  25724  plypf1  25726  dvply1  25797  pserdvlem2  25940  abelthlem9  25952  logtayllem  26167  logtayl  26168  cxpef  26173  rlimcnp2  26471  efrlim  26474  muinv  26697  bposlem5  26791  lgsval2lem  26810  lgsval4  26820  lgsval4a  26822  lgsneg  26824  lgsneg1  26825  lgsdilem  26827  lgsdir  26835  lgsne0  26838  gausslemma2dlem1a  26868  gausslemma2dlem3  26871  2lgslem3  26907  2sqnn0  26941  rplogsumlem2  26988  dchrisum0fno1  27014  rplogsum  27030  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  padicabv  27133  ostth1  27136  ostth3  27141  axlowdim  28219  vtxval  28260  iedgval  28261  funvtxdmge2val  28271  funiedgdmge2val  28272  funvtxdm2val  28273  funiedgdm2val  28274  snstrvtxval  28297  snstriedgval  28298  crctcshwlkn0lem3  29066  crctcsh  29078  clwlkclwwlklem2fv2  29249  eucrct2eupth  29498  pmtridfv1  32254  pmtridfv2  32255  psgnfzto1stlem  32259  elrspunsn  32547  gsummoncoe1fzo  32668  smattr  32779  smatbl  32780  smatbr  32781  1smat1  32784  submatminr1  32790  madjusmdetlem1  32807  madjusmdetlem2  32808  xrge0iifcv  32914  xrge0iif1  32918  ind0  33016  esumpinfval  33071  sigaclfu2  33119  eulerpartlemgs2  33379  ballotlemrv2  33520  signswmnd  33568  signswlid  33570  signsvtp  33594  signlem0  33598  ex-sategoelelomsuc  34417  ex-sategoelel12  34418  mrsubcn  34510  bcneg1  34706  bccolsum  34709  dfrdg2  34767  dfrdg4  34923  unblimceq0lem  35382  unbdqndv2lem2  35386  finxpreclem3  36274  finxpreclem5  36276  poimirlem1  36489  poimirlem2  36490  poimirlem7  36495  poimirlem10  36498  poimirlem11  36499  poimirlem16  36504  poimirlem17  36505  poimirlem20  36508  poimirlem24  36512  mblfinlem2  36526  itg2addnclem2  36540  ibladdnclem  36544  ftc1anclem6  36566  ftc1anclem8  36568  fdc  36613  heiborlem6  36684  cdleme31fv2  39264  cdlemefr27cl  39274  sticksstones10  40971  sticksstones12a  40973  sticksstones12  40974  metakunt21  41005  metakunt27  41011  metakunt28  41012  metakunt29  41013  metakunt30  41014  metakunt31  41015  evlsbagval  41138  selvvvval  41157  fsuppssind  41165  mhpind  41166  prjspner1  41368  kelac1  41805  flcidc  41916  oe0suclim  42027  oe0rif  42035  cantnfub  42071  cantnfresb  42074  tfsconcatfv  42091  sqrtcval  42392  relexp01min  42464  relexpxpmin  42468  clsk1indlem0  42792  refsum2cnlem1  43721  upbdrech2  44018  ssfiunibd  44019  ioondisj2  44206  limsup10exlem  44488  icccncfext  44603  cncfiooicclem1  44609  cncfioobdlem  44612  dvnxpaek  44658  dvnprodlem1  44662  ditgeqiooicc  44676  iblcncfioo  44694  volioore  44706  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem40  44863  fourierdlem56  44878  fourierdlem65  44887  fourierdlem66  44888  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem78  44900  fourierdlem79  44901  fourierdlem81  44903  fourierdlem82  44904  fourierdlem97  44919  fourierdlem103  44925  fourierdlem104  44926  sqwvfoura  44944  sqwvfourb  44945  fourierswlem  44946  fouriersw  44947  etransclem4  44954  etransclem14  44964  etransclem20  44970  etransclem22  44972  etransclem24  44974  etransclem25  44975  etransclem31  44981  etransclem32  44982  etransclem35  44985  sge0reval  45088  sge0sn  45095  nnfoctbdjlem  45171  isomenndlem  45246  ovnn0val  45267  ovnsubaddlem1  45286  hoidmvn0val  45300  hsphoidmvle2  45301  hsphoidmvle  45302  hoidmvval0  45303  hoidmv1lelem2  45308  hoidmvlelem2  45312  hoidmvlelem3  45313  ovnhoilem1  45317  hspmbllem1  45342  hspmbllem2  45343  volico2  45357  ovolval2lem  45359  ovnsubadd2lem  45361  ovolval4lem1  45365  ovnovollem3  45374  vonioo  45398  vonicc  45401  prproropf1olem3  46173  fdmdifeqresdif  47017  dig1  47294  dignn0flhalflem1  47301  itcoval1  47349  itcoval2  47350  itcoval3  47351  itcovalsuc  47353  ackvalsuc1mpt  47364