Theorem iffalsed 4502

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540  ifcif 4491

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4492

This theorem is referenced by:  ifeqor  4543  ifnot  4544  ifan  4545  somincom  6110  partfun  6668  mpodifsnif  7507  tz7.44-2  8378  tz7.44-3  8379  unxpdomlem2  9205  sniffsupp  9358  unwdomg  9544  cantnfp1lem1  9638  cantnfp1lem3  9640  cantnflem1d  9648  ttrcltr  9676  updjudhcoinrg  9893  ttukeylem7  10475  canthp1lem2  10613  pwfseqlem3  10620  xmulneg1  13236  rexmul  13238  xmulpnf1  13241  fzprval  13553  expnnval  14036  expneg  14041  tpf1ofv1  14469  tpf1ofv2  14470  ccatval2  14550  ccatalpha  14565  swrdnd  14626  swrdnd2  14627  swrd0  14630  swrdccatin2  14701  relexpsucnnr  14998  relexp1g  14999  sgnp  15063  sgnn  15067  absmax  15303  sumss2  15699  fsumsplit  15714  fprodntriv  15915  fprodsplit  15939  ef0lem  16051  rpnnen2lem9  16197  sadadd2  16437  eucalgf  16560  eucalginv  16561  eucalglt  16562  iserodd  16813  pcmpt  16870  pcmpt2  16871  ramtub  16990  prmo1  17015  fvprif  17531  gsumval2a  18619  mgm2nsgrplem2  18853  mgm2nsgrplem3  18854  sgrp2nmndlem3  18859  mulgnn  19014  mulgnegnn  19023  symgextfv  19355  pmtrprfv3  19391  pmtrdifellem4  19416  pmtrprfval  19424  pmtrprfvalrn  19425  odlem2  19476  dfod2  19501  gsumval3a  19840  gsumzsplit  19864  dmdprdsplitlem  19976  ablsimpgfind  20049  abvtrivd  20748  uvcvv0  21706  uvcff  21707  psrlidm  21878  psrridm  21879  mvrcl  21908  mplmon  21949  mplmonmul  21950  mplcoe1  21951  mplcoe5  21954  evlslem3  21994  coe1tmfv2  22168  cply1coe0  22195  cply1coe0bi  22196  gsummoncoe1  22202  mulmarep1gsum1  22467  1marepvsma1  22477  mdetunilem2  22507  mdetunilem9  22514  maducoeval2  22534  symgmatr01lem  22547  gsummatr01lem3  22551  gsummatr01lem4  22552  gsummatr01  22553  m2cpm  22635  m2cpminvid2lem  22648  pmatcollpw3fi1lem1  22680  mp2pm2mplem4  22703  chfacffsupp  22750  chfacfscmul0  22752  chfacfpmmul0  22756  ptpjpre2  23474  ptopn2  23478  xkopt  23549  tsmssplit  24046  xrsxmet  24705  htpycc  24886  pco1  24922  pcohtpylem  24926  pcoass  24931  pcorevlem  24933  ovolunlem1a  25404  ovolunlem1  25405  ovolicc1  25424  itg11  25599  mbfi1flim  25631  itg2split  25657  itg2cnlem1  25669  itgeq2  25686  iblss  25713  itgss2  25721  itgss3  25723  itgless  25725  ibladdlem  25728  itgaddlem1  25731  itggt0  25752  itgcn  25753  dvexp2  25865  lhop2  25927  deg1add  26015  ig1pval3  26090  ply1termlem  26115  plyeq0lem  26122  plypf1  26124  dvply1  26198  pserdvlem2  26345  abelthlem9  26357  logtayllem  26575  logtayl  26576  cxpef  26581  rlimcnp2  26883  efrlim  26886  efrlimOLD  26887  muinv  27110  bposlem5  27206  lgsval2lem  27225  lgsval4  27235  lgsval4a  27237  lgsneg  27239  lgsneg1  27240  lgsdilem  27242  lgsdir  27250  lgsne0  27253  gausslemma2dlem1a  27283  gausslemma2dlem3  27286  2lgslem3  27322  2sqnn0  27356  rplogsumlem2  27403  dchrisum0fno1  27429  rplogsum  27445  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  padicabv  27548  ostth1  27551  ostth3  27556  expsnnval  28319  axlowdim  28895  vtxval  28934  iedgval  28935  funvtxdmge2val  28945  funiedgdmge2val  28946  funvtxdm2val  28947  funiedgdm2val  28948  snstrvtxval  28971  snstriedgval  28972  crctcshwlkn0lem3  29749  crctcsh  29761  clwlkclwwlklem2fv2  29932  eucrct2eupth  30181  fmptunsnop  32630  ind0  32788  ccatws1f1o  32880  pmtridfv1  33059  pmtridfv2  33060  psgnfzto1stlem  33064  elrgspnlem2  33201  elrgspnlem3  33202  elrgspnlem4  33203  elrspunsn  33407  gsummoncoe1fzo  33570  rtelextdg2lem  33723  2sqr3minply  33777  cos9thpiminply  33785  smattr  33796  smatbl  33797  smatbr  33798  1smat1  33801  submatminr1  33807  madjusmdetlem1  33824  madjusmdetlem2  33825  xrge0iifcv  33931  xrge0iif1  33935  esumpinfval  34070  sigaclfu2  34118  eulerpartlemgs2  34378  ballotlemrv2  34520  signswmnd  34555  signswlid  34557  signsvtp  34581  signlem0  34585  ex-sategoelelomsuc  35420  ex-sategoelel12  35421  mrsubcn  35513  bcneg1  35730  bccolsum  35733  dfrdg2  35790  dfrdg4  35946  unblimceq0lem  36501  unbdqndv2lem2  36505  finxpreclem3  37388  finxpreclem5  37390  poimirlem1  37622  poimirlem2  37623  poimirlem7  37628  poimirlem10  37631  poimirlem11  37632  poimirlem16  37637  poimirlem17  37638  poimirlem20  37641  poimirlem24  37645  mblfinlem2  37659  itg2addnclem2  37673  ibladdnclem  37677  ftc1anclem6  37699  ftc1anclem8  37701  fdc  37746  heiborlem6  37817  cdleme31fv2  40394  cdlemefr27cl  40404  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  evlsbagval  42561  selvvvval  42580  fsuppssind  42588  mhpind  42589  prjspner1  42621  kelac1  43059  flcidc  43166  oe0suclim  43273  oe0rif  43281  cantnfub  43317  cantnfresb  43320  tfsconcatfv  43337  sqrtcval  43637  relexp01min  43709  relexpxpmin  43713  clsk1indlem0  44037  refsum2cnlem1  45038  upbdrech2  45313  ssfiunibd  45314  ioondisj2  45498  limsup10exlem  45777  icccncfext  45892  cncfiooicclem1  45898  cncfioobdlem  45901  dvnxpaek  45947  dvnprodlem1  45951  ditgeqiooicc  45965  iblcncfioo  45983  volioore  45995  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem40  46152  fourierdlem56  46167  fourierdlem65  46176  fourierdlem66  46177  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem78  46189  fourierdlem79  46190  fourierdlem81  46192  fourierdlem82  46193  fourierdlem97  46208  fourierdlem103  46214  fourierdlem104  46215  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  etransclem4  46243  etransclem14  46253  etransclem20  46259  etransclem22  46261  etransclem24  46263  etransclem25  46264  etransclem31  46270  etransclem32  46271  etransclem35  46274  sge0reval  46377  sge0sn  46384  nnfoctbdjlem  46460  isomenndlem  46535  ovnn0val  46556  ovnsubaddlem1  46575  hoidmvn0val  46589  hsphoidmvle2  46590  hsphoidmvle  46591  hoidmvval0  46592  hoidmv1lelem2  46597  hoidmvlelem2  46601  hoidmvlelem3  46602  ovnhoilem1  46606  hspmbllem1  46631  hspmbllem2  46632  volico2  46646  ovolval2lem  46648  ovnsubadd2lem  46650  ovolval4lem1  46654  ovnovollem3  46663  vonioo  46687  vonicc  46690  prproropf1olem3  47510  fdmdifeqresdif  48334  dig1  48601  dignn0flhalflem1  48608  itcoval1  48656  itcoval2  48657  itcoval3  48658  itcovalsuc  48660  ackvalsuc1mpt  48671