Theorem iffalsed 4489

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4479

This theorem is referenced by:  ifeqor  4530  ifnot  4531  ifan  4532  somincom  6087  partfun  6633  mpodifsnif  7468  tz7.44-2  8336  tz7.44-3  8337  unxpdomlem2  9156  sniffsupp  9309  unwdomg  9495  cantnfp1lem1  9593  cantnfp1lem3  9595  cantnflem1d  9603  ttrcltr  9631  updjudhcoinrg  9848  ttukeylem7  10428  canthp1lem2  10566  pwfseqlem3  10573  xmulneg1  13189  rexmul  13191  xmulpnf1  13194  fzprval  13506  expnnval  13989  expneg  13994  tpf1ofv1  14422  tpf1ofv2  14423  ccatval2  14503  ccatalpha  14518  swrdnd  14579  swrdnd2  14580  swrd0  14583  swrdccatin2  14653  relexpsucnnr  14950  relexp1g  14951  sgnp  15015  sgnn  15019  absmax  15255  sumss2  15651  fsumsplit  15666  fprodntriv  15867  fprodsplit  15891  ef0lem  16003  rpnnen2lem9  16149  sadadd2  16389  eucalgf  16512  eucalginv  16513  eucalglt  16514  iserodd  16765  pcmpt  16822  pcmpt2  16823  ramtub  16942  prmo1  16967  fvprif  17483  gsumval2a  18577  mgm2nsgrplem2  18811  mgm2nsgrplem3  18812  sgrp2nmndlem3  18817  mulgnn  18972  mulgnegnn  18981  symgextfv  19315  pmtrprfv3  19351  pmtrdifellem4  19376  pmtrprfval  19384  pmtrprfvalrn  19385  odlem2  19436  dfod2  19461  gsumval3a  19800  gsumzsplit  19824  dmdprdsplitlem  19936  ablsimpgfind  20009  abvtrivd  20735  uvcvv0  21715  uvcff  21716  psrlidm  21887  psrridm  21888  mvrcl  21917  mplmon  21958  mplmonmul  21959  mplcoe1  21960  mplcoe5  21963  evlslem3  22003  coe1tmfv2  22177  cply1coe0  22204  cply1coe0bi  22205  gsummoncoe1  22211  mulmarep1gsum1  22476  1marepvsma1  22486  mdetunilem2  22516  mdetunilem9  22523  maducoeval2  22543  symgmatr01lem  22556  gsummatr01lem3  22560  gsummatr01lem4  22561  gsummatr01  22562  m2cpm  22644  m2cpminvid2lem  22657  pmatcollpw3fi1lem1  22689  mp2pm2mplem4  22712  chfacffsupp  22759  chfacfscmul0  22761  chfacfpmmul0  22765  ptpjpre2  23483  ptopn2  23487  xkopt  23558  tsmssplit  24055  xrsxmet  24714  htpycc  24895  pco1  24931  pcohtpylem  24935  pcoass  24940  pcorevlem  24942  ovolunlem1a  25413  ovolunlem1  25414  ovolicc1  25433  itg11  25608  mbfi1flim  25640  itg2split  25666  itg2cnlem1  25678  itgeq2  25695  iblss  25722  itgss2  25730  itgss3  25732  itgless  25734  ibladdlem  25737  itgaddlem1  25740  itggt0  25761  itgcn  25762  dvexp2  25874  lhop2  25936  deg1add  26024  ig1pval3  26099  ply1termlem  26124  plyeq0lem  26131  plypf1  26133  dvply1  26207  pserdvlem2  26354  abelthlem9  26366  logtayllem  26584  logtayl  26585  cxpef  26590  rlimcnp2  26892  efrlim  26895  efrlimOLD  26896  muinv  27119  bposlem5  27215  lgsval2lem  27234  lgsval4  27244  lgsval4a  27246  lgsneg  27248  lgsneg1  27249  lgsdilem  27251  lgsdir  27259  lgsne0  27262  gausslemma2dlem1a  27292  gausslemma2dlem3  27295  2lgslem3  27331  2sqnn0  27365  rplogsumlem2  27412  dchrisum0fno1  27438  rplogsum  27454  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  padicabv  27557  ostth1  27560  ostth3  27565  expsnnval  28336  axlowdim  28924  vtxval  28963  iedgval  28964  funvtxdmge2val  28974  funiedgdmge2val  28975  funvtxdm2val  28976  funiedgdm2val  28977  snstrvtxval  29000  snstriedgval  29001  crctcshwlkn0lem3  29775  crctcsh  29787  clwlkclwwlklem2fv2  29958  eucrct2eupth  30207  fmptunsnop  32656  ind0  32814  ccatws1f1o  32906  pmtridfv1  33050  pmtridfv2  33051  psgnfzto1stlem  33055  elrgspnlem2  33196  elrgspnlem3  33197  elrgspnlem4  33198  elrspunsn  33379  gsummoncoe1fzo  33542  rtelextdg2lem  33695  2sqr3minply  33749  cos9thpiminply  33757  smattr  33768  smatbl  33769  smatbr  33770  1smat1  33773  submatminr1  33779  madjusmdetlem1  33796  madjusmdetlem2  33797  xrge0iifcv  33903  xrge0iif1  33907  esumpinfval  34042  sigaclfu2  34090  eulerpartlemgs2  34350  ballotlemrv2  34492  signswmnd  34527  signswlid  34529  signsvtp  34553  signlem0  34557  ex-sategoelelomsuc  35401  ex-sategoelel12  35402  mrsubcn  35494  bcneg1  35711  bccolsum  35714  dfrdg2  35771  dfrdg4  35927  unblimceq0lem  36482  unbdqndv2lem2  36486  finxpreclem3  37369  finxpreclem5  37371  poimirlem1  37603  poimirlem2  37604  poimirlem7  37609  poimirlem10  37612  poimirlem11  37613  poimirlem16  37618  poimirlem17  37619  poimirlem20  37622  poimirlem24  37626  mblfinlem2  37640  itg2addnclem2  37654  ibladdnclem  37658  ftc1anclem6  37680  ftc1anclem8  37682  fdc  37727  heiborlem6  37798  cdleme31fv2  40375  cdlemefr27cl  40385  sticksstones10  42131  sticksstones12a  42133  sticksstones12  42134  evlsbagval  42542  selvvvval  42561  fsuppssind  42569  mhpind  42570  prjspner1  42602  kelac1  43039  flcidc  43146  oe0suclim  43253  oe0rif  43261  cantnfub  43297  cantnfresb  43300  tfsconcatfv  43317  sqrtcval  43617  relexp01min  43689  relexpxpmin  43693  clsk1indlem0  44017  refsum2cnlem1  45018  upbdrech2  45293  ssfiunibd  45294  ioondisj2  45478  limsup10exlem  45757  icccncfext  45872  cncfiooicclem1  45878  cncfioobdlem  45881  dvnxpaek  45927  dvnprodlem1  45931  ditgeqiooicc  45945  iblcncfioo  45963  volioore  45975  dirkercncflem2  46089  dirkercncflem4  46091  fourierdlem40  46132  fourierdlem56  46147  fourierdlem65  46156  fourierdlem66  46157  fourierdlem73  46164  fourierdlem74  46165  fourierdlem75  46166  fourierdlem78  46169  fourierdlem79  46170  fourierdlem81  46172  fourierdlem82  46173  fourierdlem97  46188  fourierdlem103  46194  fourierdlem104  46195  sqwvfoura  46213  sqwvfourb  46214  fourierswlem  46215  fouriersw  46216  etransclem4  46223  etransclem14  46233  etransclem20  46239  etransclem22  46241  etransclem24  46243  etransclem25  46244  etransclem31  46250  etransclem32  46251  etransclem35  46254  sge0reval  46357  sge0sn  46364  nnfoctbdjlem  46440  isomenndlem  46515  ovnn0val  46536  ovnsubaddlem1  46555  hoidmvn0val  46569  hsphoidmvle2  46570  hsphoidmvle  46571  hoidmvval0  46572  hoidmv1lelem2  46577  hoidmvlelem2  46581  hoidmvlelem3  46582  ovnhoilem1  46586  hspmbllem1  46611  hspmbllem2  46612  volico2  46626  ovolval2lem  46628  ovnsubadd2lem  46630  ovolval4lem1  46634  ovnovollem3  46643  vonioo  46667  vonicc  46670  prproropf1olem3  47493  fdmdifeqresdif  48330  dig1  48597  dignn0flhalflem1  48604  itcoval1  48652  itcoval2  48653  itcoval3  48654  itcovalsuc  48656  ackvalsuc1mpt  48667