Theorem iffalsed 4398

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1525  ifcif 4387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ex 1766  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-if 4388

This theorem is referenced by:  ifeqor  4436  ifnot  4437  ifan  4438  somincom  5877  mpodifsnif  7130  tz7.44-2  7902  tz7.44-3  7903  unxpdomlem2  8576  sniffsupp  8726  unwdomg  8901  cantnfp1lem1  8994  cantnfp1lem3  8996  cantnflem1d  9004  updjudhcoinrg  9215  ttukeylem7  9790  canthp1lem2  9928  pwfseqlem3  9935  xmulneg1  12516  rexmul  12518  xmulpnf1  12521  fzprval  12822  expnnval  13286  expneg  13291  ccatval2  13780  ccatalpha  13795  swrdnd  13856  swrdnd2  13857  swrd0  13860  swrdccatin2  13931  relexpsucnnr  14222  relexp1g  14223  sgnp  14287  sgnn  14291  absmax  14527  sumss2  14920  fsumsplit  14934  fprodntriv  15133  fprodsplit  15157  ef0lem  15269  rpnnen2lem9  15412  sadadd2  15646  eucalgf  15760  eucalginv  15761  eucalglt  15762  iserodd  16005  pcmpt  16061  pcmpt2  16062  ramtub  16181  prmo1  16206  fvprif  16667  gsumval2a  17722  mgm2nsgrplem2  17849  mgm2nsgrplem3  17850  sgrp2nmndlem3  17855  mulgnn  17993  mulgnegnn  17997  symgextfv  18281  pmtrprfv3  18317  pmtrdifellem4  18342  pmtrprfval  18350  pmtrprfvalrn  18351  odlem2  18402  dfod2  18425  gsumval3a  18748  gsumzsplit  18771  dmdprdsplitlem  18880  abvtrivd  19305  psrlidm  19875  psrridm  19876  mvrcl  19921  mplmon  19935  mplmonmul  19936  mplcoe1  19937  mplcoe5  19940  evlslem3  19984  coe1tmfv2  20130  cply1coe0  20154  cply1coe0bi  20155  gsummoncoe1  20159  uvcvv0  20620  uvcff  20621  mulmarep1gsum1  20870  1marepvsma1  20880  mdetunilem2  20910  mdetunilem9  20917  maducoeval2  20937  symgmatr01lem  20950  gsummatr01lem3  20954  gsummatr01lem4  20955  gsummatr01  20956  m2cpm  21037  m2cpminvid2lem  21050  pmatcollpw3fi1lem1  21082  mp2pm2mplem4  21105  chfacffsupp  21152  chfacfscmul0  21154  chfacfpmmul0  21158  ptpjpre2  21876  ptopn2  21880  xkopt  21951  tsmssplit  22447  xrsxmet  23104  htpycc  23271  pco1  23306  pcohtpylem  23310  pcoass  23315  pcorevlem  23317  ovolunlem1a  23784  ovolunlem1  23785  ovolicc1  23804  itg11  23979  mbfi1flim  24011  itg2split  24037  itg2cnlem1  24049  itgeq2  24065  iblss  24092  itgss2  24100  itgss3  24102  itgless  24104  ibladdlem  24107  itgaddlem1  24110  itggt0  24129  itgcn  24130  dvexp2  24238  lhop2  24299  deg1add  24384  ig1pval3  24455  ply1termlem  24480  plyeq0lem  24487  plypf1  24489  dvply1  24560  pserdvlem2  24703  abelthlem9  24715  logtayllem  24927  logtayl  24928  cxpef  24933  rlimcnp2  25230  efrlim  25233  muinv  25456  bposlem5  25550  lgsval2lem  25569  lgsval4  25579  lgsval4a  25581  lgsneg  25583  lgsneg1  25584  lgsdilem  25586  lgsdir  25594  lgsne0  25597  gausslemma2dlem1a  25627  gausslemma2dlem3  25630  2lgslem3  25666  2sqnn0  25700  rplogsumlem2  25747  dchrisum0fno1  25773  rplogsum  25789  pntrlog2bndlem4  25842  pntrlog2bndlem5  25843  padicabv  25892  ostth1  25895  ostth3  25900  axlowdim  26434  vtxval  26472  iedgval  26473  funvtxdmge2val  26483  funiedgdmge2val  26484  funvtxdm2val  26485  funiedgdm2val  26486  snstrvtxval  26509  snstriedgval  26510  crctcshwlkn0lem3  27276  crctcsh  27288  clwlkclwwlklem2fv2  27460  eucrct2eupth  27710  partfun  30107  psgnfzto1stlem  30660  pmtridfv1  30667  pmtridfv2  30668  smattr  30675  smatbl  30676  smatbr  30677  1smat1  30680  submatminr1  30686  madjusmdetlem1  30703  madjusmdetlem2  30704  xrge0iifcv  30790  xrge0iif1  30794  ind0  30890  esumpinfval  30945  sigaclfu2  30993  eulerpartlemgs2  31251  ballotlemrv2  31392  signswmnd  31440  signswlid  31442  signsvtp  31466  signlem0  31470  ex-sategoelelomsuc  32283  ex-sategoelel12  32284  mrsubcn  32376  bcneg1  32578  bccolsum  32581  dfrdg2  32651  dfrdg4  33023  unblimceq0lem  33456  unbdqndv2lem2  33460  finxpreclem3  34226  finxpreclem5  34228  poimirlem1  34445  poimirlem2  34446  poimirlem7  34451  poimirlem10  34454  poimirlem11  34455  poimirlem16  34460  poimirlem17  34461  poimirlem20  34464  poimirlem24  34468  mblfinlem2  34482  itg2addnclem2  34496  ibladdnclem  34500  ftc1anclem6  34524  ftc1anclem8  34526  fdc  34573  heiborlem6  34647  cdleme31fv2  37081  cdlemefr27cl  37091  kelac1  39169  flcidc  39280  relexp01min  39564  relexpxpmin  39568  clsk1indlem0  39897  ablsimpgfind  40188  refsum2cnlem1  40854  upbdrech2  41137  ssfiunibd  41138  ioondisj2  41330  limsup10exlem  41616  icccncfext  41733  cncfiooicclem1  41739  cncfioobdlem  41742  dvnxpaek  41790  dvnprodlem1  41794  ditgeqiooicc  41808  iblcncfioo  41826  volioore  41839  dirkercncflem2  41953  dirkercncflem4  41955  fourierdlem40  41996  fourierdlem56  42011  fourierdlem65  42020  fourierdlem66  42021  fourierdlem73  42028  fourierdlem74  42029  fourierdlem75  42030  fourierdlem78  42033  fourierdlem79  42034  fourierdlem81  42036  fourierdlem82  42037  fourierdlem97  42052  fourierdlem103  42058  fourierdlem104  42059  sqwvfoura  42077  sqwvfourb  42078  fourierswlem  42079  fouriersw  42080  etransclem4  42087  etransclem14  42097  etransclem20  42103  etransclem22  42105  etransclem24  42107  etransclem25  42108  etransclem31  42114  etransclem32  42115  etransclem35  42118  sge0reval  42218  sge0sn  42225  nnfoctbdjlem  42301  isomenndlem  42376  ovnn0val  42397  ovnsubaddlem1  42416  hoidmvn0val  42430  hsphoidmvle2  42431  hsphoidmvle  42432  hoidmvval0  42433  hoidmv1lelem2  42438  hoidmvlelem2  42442  hoidmvlelem3  42443  ovnhoilem1  42447  hspmbllem1  42472  hspmbllem2  42473  volico2  42487  ovolval2lem  42489  ovnsubadd2lem  42491  ovolval4lem1  42495  ovnovollem3  42504  vonioo  42528  vonicc  42531  prproropf1olem3  43171  fdmdifeqresdif  43890  dig1  44171  dignn0flhalflem1  44178