Theorem iffalsed 4541

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536  ifcif 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-if 4531

This theorem is referenced by:  ifeqor  4581  ifnot  4582  ifan  4583  somincom  6156  partfun  6715  mpodifsnif  7547  tz7.44-2  8445  tz7.44-3  8446  unxpdomlem2  9284  sniffsupp  9437  unwdomg  9621  cantnfp1lem1  9715  cantnfp1lem3  9717  cantnflem1d  9725  ttrcltr  9753  updjudhcoinrg  9970  ttukeylem7  10552  canthp1lem2  10690  pwfseqlem3  10697  xmulneg1  13307  rexmul  13309  xmulpnf1  13312  fzprval  13621  expnnval  14101  expneg  14106  tpf1ofv1  14532  tpf1ofv2  14533  ccatval2  14612  ccatalpha  14627  swrdnd  14688  swrdnd2  14689  swrd0  14692  swrdccatin2  14763  relexpsucnnr  15060  relexp1g  15061  sgnp  15125  sgnn  15129  absmax  15364  sumss2  15758  fsumsplit  15773  fprodntriv  15974  fprodsplit  15998  ef0lem  16110  rpnnen2lem9  16254  sadadd2  16493  eucalgf  16616  eucalginv  16617  eucalglt  16618  iserodd  16868  pcmpt  16925  pcmpt2  16926  ramtub  17045  prmo1  17070  fvprif  17607  gsumval2a  18710  mgm2nsgrplem2  18944  mgm2nsgrplem3  18945  sgrp2nmndlem3  18950  mulgnn  19105  mulgnegnn  19114  symgextfv  19450  pmtrprfv3  19486  pmtrdifellem4  19511  pmtrprfval  19519  pmtrprfvalrn  19520  odlem2  19571  dfod2  19596  gsumval3a  19935  gsumzsplit  19959  dmdprdsplitlem  20071  ablsimpgfind  20144  abvtrivd  20849  uvcvv0  21827  uvcff  21828  psrlidm  21999  psrridm  22000  mvrcl  22029  mplmon  22070  mplmonmul  22071  mplcoe1  22072  mplcoe5  22075  evlslem3  22121  coe1tmfv2  22293  cply1coe0  22320  cply1coe0bi  22321  gsummoncoe1  22327  mulmarep1gsum1  22594  1marepvsma1  22604  mdetunilem2  22634  mdetunilem9  22641  maducoeval2  22661  symgmatr01lem  22674  gsummatr01lem3  22678  gsummatr01lem4  22679  gsummatr01  22680  m2cpm  22762  m2cpminvid2lem  22775  pmatcollpw3fi1lem1  22807  mp2pm2mplem4  22830  chfacffsupp  22877  chfacfscmul0  22879  chfacfpmmul0  22883  ptpjpre2  23603  ptopn2  23607  xkopt  23678  tsmssplit  24175  xrsxmet  24844  htpycc  25025  pco1  25061  pcohtpylem  25065  pcoass  25070  pcorevlem  25072  ovolunlem1a  25544  ovolunlem1  25545  ovolicc1  25564  itg11  25739  mbfi1flim  25772  itg2split  25798  itg2cnlem1  25810  itgeq2  25827  iblss  25854  itgss2  25862  itgss3  25864  itgless  25866  ibladdlem  25869  itgaddlem1  25872  itggt0  25893  itgcn  25894  dvexp2  26006  lhop2  26068  deg1add  26156  ig1pval3  26231  ply1termlem  26256  plyeq0lem  26263  plypf1  26265  dvply1  26339  pserdvlem2  26486  abelthlem9  26498  logtayllem  26715  logtayl  26716  cxpef  26721  rlimcnp2  27023  efrlim  27026  efrlimOLD  27027  muinv  27250  bposlem5  27346  lgsval2lem  27365  lgsval4  27375  lgsval4a  27377  lgsneg  27379  lgsneg1  27380  lgsdilem  27382  lgsdir  27390  lgsne0  27393  gausslemma2dlem1a  27423  gausslemma2dlem3  27426  2lgslem3  27462  2sqnn0  27496  rplogsumlem2  27543  dchrisum0fno1  27569  rplogsum  27585  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  padicabv  27688  ostth1  27691  ostth3  27696  expsnnval  28423  axlowdim  28990  vtxval  29031  iedgval  29032  funvtxdmge2val  29042  funiedgdmge2val  29043  funvtxdm2val  29044  funiedgdm2val  29045  snstrvtxval  29068  snstriedgval  29069  crctcshwlkn0lem3  29841  crctcsh  29853  clwlkclwwlklem2fv2  30024  eucrct2eupth  30273  fmptunsnop  32714  ccatws1f1o  32920  pmtridfv1  33097  pmtridfv2  33098  psgnfzto1stlem  33102  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  elrspunsn  33436  gsummoncoe1fzo  33597  rtelextdg2lem  33731  2sqr3minply  33752  smattr  33759  smatbl  33760  smatbr  33761  1smat1  33764  submatminr1  33770  madjusmdetlem1  33787  madjusmdetlem2  33788  xrge0iifcv  33894  xrge0iif1  33898  ind0  33998  esumpinfval  34053  sigaclfu2  34101  eulerpartlemgs2  34361  ballotlemrv2  34502  signswmnd  34550  signswlid  34552  signsvtp  34576  signlem0  34580  ex-sategoelelomsuc  35410  ex-sategoelel12  35411  mrsubcn  35503  bcneg1  35715  bccolsum  35718  dfrdg2  35776  dfrdg4  35932  unblimceq0lem  36488  unbdqndv2lem2  36492  finxpreclem3  37375  finxpreclem5  37377  poimirlem1  37607  poimirlem2  37608  poimirlem7  37613  poimirlem10  37616  poimirlem11  37617  poimirlem16  37622  poimirlem17  37623  poimirlem20  37626  poimirlem24  37630  mblfinlem2  37644  itg2addnclem2  37658  ibladdnclem  37662  ftc1anclem6  37684  ftc1anclem8  37686  fdc  37731  heiborlem6  37802  cdleme31fv2  40375  cdlemefr27cl  40385  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  metakunt21  42206  metakunt27  42212  metakunt28  42213  metakunt29  42214  metakunt30  42215  metakunt31  42216  evlsbagval  42552  selvvvval  42571  fsuppssind  42579  mhpind  42580  prjspner1  42612  kelac1  43051  flcidc  43158  oe0suclim  43266  oe0rif  43274  cantnfub  43310  cantnfresb  43313  tfsconcatfv  43330  sqrtcval  43630  relexp01min  43702  relexpxpmin  43706  clsk1indlem0  44030  refsum2cnlem1  44974  upbdrech2  45258  ssfiunibd  45259  ioondisj2  45445  limsup10exlem  45727  icccncfext  45842  cncfiooicclem1  45848  cncfioobdlem  45851  dvnxpaek  45897  dvnprodlem1  45901  ditgeqiooicc  45915  iblcncfioo  45933  volioore  45945  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem40  46102  fourierdlem56  46117  fourierdlem65  46126  fourierdlem66  46127  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem78  46139  fourierdlem79  46140  fourierdlem81  46142  fourierdlem82  46143  fourierdlem97  46158  fourierdlem103  46164  fourierdlem104  46165  sqwvfoura  46183  sqwvfourb  46184  fourierswlem  46185  fouriersw  46186  etransclem4  46193  etransclem14  46203  etransclem20  46209  etransclem22  46211  etransclem24  46213  etransclem25  46214  etransclem31  46220  etransclem32  46221  etransclem35  46224  sge0reval  46327  sge0sn  46334  nnfoctbdjlem  46410  isomenndlem  46485  ovnn0val  46506  ovnsubaddlem1  46525  hoidmvn0val  46539  hsphoidmvle2  46540  hsphoidmvle  46541  hoidmvval0  46542  hoidmv1lelem2  46547  hoidmvlelem2  46551  hoidmvlelem3  46552  ovnhoilem1  46556  hspmbllem1  46581  hspmbllem2  46582  volico2  46596  ovolval2lem  46598  ovnsubadd2lem  46600  ovolval4lem1  46604  ovnovollem3  46613  vonioo  46637  vonicc  46640  prproropf1olem3  47429  fdmdifeqresdif  48186  dig1  48457  dignn0flhalflem1  48464  itcoval1  48512  itcoval2  48513  itcoval3  48514  itcovalsuc  48516  ackvalsuc1mpt  48527