Theorem iffalsed 4511

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-if 4501

This theorem is referenced by:  ifeqor  4552  ifnot  4553  ifan  4554  somincom  6123  partfun  6684  mpodifsnif  7520  tz7.44-2  8419  tz7.44-3  8420  unxpdomlem2  9257  sniffsupp  9410  unwdomg  9596  cantnfp1lem1  9690  cantnfp1lem3  9692  cantnflem1d  9700  ttrcltr  9728  updjudhcoinrg  9945  ttukeylem7  10527  canthp1lem2  10665  pwfseqlem3  10672  xmulneg1  13283  rexmul  13285  xmulpnf1  13288  fzprval  13600  expnnval  14080  expneg  14085  tpf1ofv1  14513  tpf1ofv2  14514  ccatval2  14594  ccatalpha  14609  swrdnd  14670  swrdnd2  14671  swrd0  14674  swrdccatin2  14745  relexpsucnnr  15042  relexp1g  15043  sgnp  15107  sgnn  15111  absmax  15346  sumss2  15740  fsumsplit  15755  fprodntriv  15956  fprodsplit  15980  ef0lem  16092  rpnnen2lem9  16238  sadadd2  16477  eucalgf  16600  eucalginv  16601  eucalglt  16602  iserodd  16853  pcmpt  16910  pcmpt2  16911  ramtub  17030  prmo1  17055  fvprif  17573  gsumval2a  18661  mgm2nsgrplem2  18895  mgm2nsgrplem3  18896  sgrp2nmndlem3  18901  mulgnn  19056  mulgnegnn  19065  symgextfv  19397  pmtrprfv3  19433  pmtrdifellem4  19458  pmtrprfval  19466  pmtrprfvalrn  19467  odlem2  19518  dfod2  19543  gsumval3a  19882  gsumzsplit  19906  dmdprdsplitlem  20018  ablsimpgfind  20091  abvtrivd  20790  uvcvv0  21748  uvcff  21749  psrlidm  21920  psrridm  21921  mvrcl  21950  mplmon  21991  mplmonmul  21992  mplcoe1  21993  mplcoe5  21996  evlslem3  22036  coe1tmfv2  22210  cply1coe0  22237  cply1coe0bi  22238  gsummoncoe1  22244  mulmarep1gsum1  22509  1marepvsma1  22519  mdetunilem2  22549  mdetunilem9  22556  maducoeval2  22576  symgmatr01lem  22589  gsummatr01lem3  22593  gsummatr01lem4  22594  gsummatr01  22595  m2cpm  22677  m2cpminvid2lem  22690  pmatcollpw3fi1lem1  22722  mp2pm2mplem4  22745  chfacffsupp  22792  chfacfscmul0  22794  chfacfpmmul0  22798  ptpjpre2  23516  ptopn2  23520  xkopt  23591  tsmssplit  24088  xrsxmet  24747  htpycc  24928  pco1  24964  pcohtpylem  24968  pcoass  24973  pcorevlem  24975  ovolunlem1a  25447  ovolunlem1  25448  ovolicc1  25467  itg11  25642  mbfi1flim  25674  itg2split  25700  itg2cnlem1  25712  itgeq2  25729  iblss  25756  itgss2  25764  itgss3  25766  itgless  25768  ibladdlem  25771  itgaddlem1  25774  itggt0  25795  itgcn  25796  dvexp2  25908  lhop2  25970  deg1add  26058  ig1pval3  26133  ply1termlem  26158  plyeq0lem  26165  plypf1  26167  dvply1  26241  pserdvlem2  26388  abelthlem9  26400  logtayllem  26618  logtayl  26619  cxpef  26624  rlimcnp2  26926  efrlim  26929  efrlimOLD  26930  muinv  27153  bposlem5  27249  lgsval2lem  27268  lgsval4  27278  lgsval4a  27280  lgsneg  27282  lgsneg1  27283  lgsdilem  27285  lgsdir  27293  lgsne0  27296  gausslemma2dlem1a  27326  gausslemma2dlem3  27329  2lgslem3  27365  2sqnn0  27399  rplogsumlem2  27446  dchrisum0fno1  27472  rplogsum  27488  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  padicabv  27591  ostth1  27594  ostth3  27599  expsnnval  28326  axlowdim  28886  vtxval  28925  iedgval  28926  funvtxdmge2val  28936  funiedgdmge2val  28937  funvtxdm2val  28938  funiedgdm2val  28939  snstrvtxval  28962  snstriedgval  28963  crctcshwlkn0lem3  29740  crctcsh  29752  clwlkclwwlklem2fv2  29923  eucrct2eupth  30172  fmptunsnop  32623  ind0  32781  ccatws1f1o  32873  pmtridfv1  33052  pmtridfv2  33053  psgnfzto1stlem  33057  elrgspnlem2  33184  elrgspnlem3  33185  elrgspnlem4  33186  elrspunsn  33390  gsummoncoe1fzo  33553  rtelextdg2lem  33706  2sqr3minply  33760  cos9thpiminply  33768  smattr  33776  smatbl  33777  smatbr  33778  1smat1  33781  submatminr1  33787  madjusmdetlem1  33804  madjusmdetlem2  33805  xrge0iifcv  33911  xrge0iif1  33915  esumpinfval  34050  sigaclfu2  34098  eulerpartlemgs2  34358  ballotlemrv2  34500  signswmnd  34535  signswlid  34537  signsvtp  34561  signlem0  34565  ex-sategoelelomsuc  35394  ex-sategoelel12  35395  mrsubcn  35487  bcneg1  35699  bccolsum  35702  dfrdg2  35759  dfrdg4  35915  unblimceq0lem  36470  unbdqndv2lem2  36474  finxpreclem3  37357  finxpreclem5  37359  poimirlem1  37591  poimirlem2  37592  poimirlem7  37597  poimirlem10  37600  poimirlem11  37601  poimirlem16  37606  poimirlem17  37607  poimirlem20  37610  poimirlem24  37614  mblfinlem2  37628  itg2addnclem2  37642  ibladdnclem  37646  ftc1anclem6  37668  ftc1anclem8  37670  fdc  37715  heiborlem6  37786  cdleme31fv2  40358  cdlemefr27cl  40368  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  metakunt21  42184  metakunt27  42190  metakunt28  42191  metakunt29  42192  metakunt30  42193  metakunt31  42194  evlsbagval  42536  selvvvval  42555  fsuppssind  42563  mhpind  42564  prjspner1  42596  kelac1  43034  flcidc  43141  oe0suclim  43248  oe0rif  43256  cantnfub  43292  cantnfresb  43295  tfsconcatfv  43312  sqrtcval  43612  relexp01min  43684  relexpxpmin  43688  clsk1indlem0  44012  refsum2cnlem1  45009  upbdrech2  45285  ssfiunibd  45286  ioondisj2  45470  limsup10exlem  45749  icccncfext  45864  cncfiooicclem1  45870  cncfioobdlem  45873  dvnxpaek  45919  dvnprodlem1  45923  ditgeqiooicc  45937  iblcncfioo  45955  volioore  45967  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem40  46124  fourierdlem56  46139  fourierdlem65  46148  fourierdlem66  46149  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem78  46161  fourierdlem79  46162  fourierdlem81  46164  fourierdlem82  46165  fourierdlem97  46180  fourierdlem103  46186  fourierdlem104  46187  sqwvfoura  46205  sqwvfourb  46206  fourierswlem  46207  fouriersw  46208  etransclem4  46215  etransclem14  46225  etransclem20  46231  etransclem22  46233  etransclem24  46235  etransclem25  46236  etransclem31  46242  etransclem32  46243  etransclem35  46246  sge0reval  46349  sge0sn  46356  nnfoctbdjlem  46432  isomenndlem  46507  ovnn0val  46528  ovnsubaddlem1  46547  hoidmvn0val  46561  hsphoidmvle2  46562  hsphoidmvle  46563  hoidmvval0  46564  hoidmv1lelem2  46569  hoidmvlelem2  46573  hoidmvlelem3  46574  ovnhoilem1  46578  hspmbllem1  46603  hspmbllem2  46604  volico2  46618  ovolval2lem  46620  ovnsubadd2lem  46622  ovolval4lem1  46626  ovnovollem3  46635  vonioo  46659  vonicc  46662  prproropf1olem3  47467  fdmdifeqresdif  48265  dig1  48536  dignn0flhalflem1  48543  itcoval1  48591  itcoval2  48592  itcoval3  48593  itcovalsuc  48595  ackvalsuc1mpt  48606