Theorem iffalsed 4538

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541  ifcif 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-if 4528

This theorem is referenced by:  ifeqor  4578  ifnot  4579  ifan  4580  somincom  6132  partfun  6694  mpodifsnif  7519  tz7.44-2  8403  tz7.44-3  8404  unxpdomlem2  9247  sniffsupp  9391  unwdomg  9575  cantnfp1lem1  9669  cantnfp1lem3  9671  cantnflem1d  9679  ttrcltr  9707  updjudhcoinrg  9924  ttukeylem7  10506  canthp1lem2  10644  pwfseqlem3  10651  xmulneg1  13244  rexmul  13246  xmulpnf1  13249  fzprval  13558  expnnval  14026  expneg  14031  ccatval2  14524  ccatalpha  14539  swrdnd  14600  swrdnd2  14601  swrd0  14604  swrdccatin2  14675  relexpsucnnr  14968  relexp1g  14969  sgnp  15033  sgnn  15037  absmax  15272  sumss2  15668  fsumsplit  15683  fprodntriv  15882  fprodsplit  15906  ef0lem  16018  rpnnen2lem9  16161  sadadd2  16397  eucalgf  16516  eucalginv  16517  eucalglt  16518  iserodd  16764  pcmpt  16821  pcmpt2  16822  ramtub  16941  prmo1  16966  fvprif  17503  gsumval2a  18600  mgm2nsgrplem2  18796  mgm2nsgrplem3  18797  sgrp2nmndlem3  18802  mulgnn  18952  mulgnegnn  18958  symgextfv  19280  pmtrprfv3  19316  pmtrdifellem4  19341  pmtrprfval  19349  pmtrprfvalrn  19350  odlem2  19401  dfod2  19426  gsumval3a  19765  gsumzsplit  19789  dmdprdsplitlem  19901  ablsimpgfind  19974  abvtrivd  20440  uvcvv0  21336  uvcff  21337  psrlidm  21514  psrridm  21515  mvrcl  21542  mplmon  21581  mplmonmul  21582  mplcoe1  21583  mplcoe5  21586  evlslem3  21634  coe1tmfv2  21788  cply1coe0  21814  cply1coe0bi  21815  gsummoncoe1  21819  mulmarep1gsum1  22066  1marepvsma1  22076  mdetunilem2  22106  mdetunilem9  22113  maducoeval2  22133  symgmatr01lem  22146  gsummatr01lem3  22150  gsummatr01lem4  22151  gsummatr01  22152  m2cpm  22234  m2cpminvid2lem  22247  pmatcollpw3fi1lem1  22279  mp2pm2mplem4  22302  chfacffsupp  22349  chfacfscmul0  22351  chfacfpmmul0  22355  ptpjpre2  23075  ptopn2  23079  xkopt  23150  tsmssplit  23647  xrsxmet  24316  htpycc  24487  pco1  24522  pcohtpylem  24526  pcoass  24531  pcorevlem  24533  ovolunlem1a  25004  ovolunlem1  25005  ovolicc1  25024  itg11  25199  mbfi1flim  25232  itg2split  25258  itg2cnlem1  25270  itgeq2  25286  iblss  25313  itgss2  25321  itgss3  25323  itgless  25325  ibladdlem  25328  itgaddlem1  25331  itggt0  25352  itgcn  25353  dvexp2  25462  lhop2  25523  deg1add  25612  ig1pval3  25683  ply1termlem  25708  plyeq0lem  25715  plypf1  25717  dvply1  25788  pserdvlem2  25931  abelthlem9  25943  logtayllem  26158  logtayl  26159  cxpef  26164  rlimcnp2  26460  efrlim  26463  muinv  26686  bposlem5  26780  lgsval2lem  26799  lgsval4  26809  lgsval4a  26811  lgsneg  26813  lgsneg1  26814  lgsdilem  26816  lgsdir  26824  lgsne0  26827  gausslemma2dlem1a  26857  gausslemma2dlem3  26860  2lgslem3  26896  2sqnn0  26930  rplogsumlem2  26977  dchrisum0fno1  27003  rplogsum  27019  pntrlog2bndlem4  27072  pntrlog2bndlem5  27073  padicabv  27122  ostth1  27125  ostth3  27130  axlowdim  28208  vtxval  28249  iedgval  28250  funvtxdmge2val  28260  funiedgdmge2val  28261  funvtxdm2val  28262  funiedgdm2val  28263  snstrvtxval  28286  snstriedgval  28287  crctcshwlkn0lem3  29055  crctcsh  29067  clwlkclwwlklem2fv2  29238  eucrct2eupth  29487  pmtridfv1  32241  pmtridfv2  32242  psgnfzto1stlem  32246  elrspunsn  32535  gsummoncoe1fzo  32656  smattr  32767  smatbl  32768  smatbr  32769  1smat1  32772  submatminr1  32778  madjusmdetlem1  32795  madjusmdetlem2  32796  xrge0iifcv  32902  xrge0iif1  32906  ind0  33004  esumpinfval  33059  sigaclfu2  33107  eulerpartlemgs2  33367  ballotlemrv2  33508  signswmnd  33556  signswlid  33558  signsvtp  33582  signlem0  33586  ex-sategoelelomsuc  34405  ex-sategoelel12  34406  mrsubcn  34498  bcneg1  34694  bccolsum  34697  dfrdg2  34755  dfrdg4  34911  unblimceq0lem  35370  unbdqndv2lem2  35374  finxpreclem3  36262  finxpreclem5  36264  poimirlem1  36477  poimirlem2  36478  poimirlem7  36483  poimirlem10  36486  poimirlem11  36487  poimirlem16  36492  poimirlem17  36493  poimirlem20  36496  poimirlem24  36500  mblfinlem2  36514  itg2addnclem2  36528  ibladdnclem  36532  ftc1anclem6  36554  ftc1anclem8  36556  fdc  36601  heiborlem6  36672  cdleme31fv2  39252  cdlemefr27cl  39262  sticksstones10  40959  sticksstones12a  40961  sticksstones12  40962  metakunt21  40993  metakunt27  40999  metakunt28  41000  metakunt29  41001  metakunt30  41002  metakunt31  41003  evlsbagval  41135  selvvvval  41154  fsuppssind  41162  mhpind  41163  prjspner1  41364  kelac1  41790  flcidc  41901  oe0suclim  42012  oe0rif  42020  cantnfub  42056  cantnfresb  42059  tfsconcatfv  42076  sqrtcval  42377  relexp01min  42449  relexpxpmin  42453  clsk1indlem0  42777  refsum2cnlem1  43706  upbdrech2  44004  ssfiunibd  44005  ioondisj2  44192  limsup10exlem  44474  icccncfext  44589  cncfiooicclem1  44595  cncfioobdlem  44598  dvnxpaek  44644  dvnprodlem1  44648  ditgeqiooicc  44662  iblcncfioo  44680  volioore  44692  dirkercncflem2  44806  dirkercncflem4  44808  fourierdlem40  44849  fourierdlem56  44864  fourierdlem65  44873  fourierdlem66  44874  fourierdlem73  44881  fourierdlem74  44882  fourierdlem75  44883  fourierdlem78  44886  fourierdlem79  44887  fourierdlem81  44889  fourierdlem82  44890  fourierdlem97  44905  fourierdlem103  44911  fourierdlem104  44912  sqwvfoura  44930  sqwvfourb  44931  fourierswlem  44932  fouriersw  44933  etransclem4  44940  etransclem14  44950  etransclem20  44956  etransclem22  44958  etransclem24  44960  etransclem25  44961  etransclem31  44967  etransclem32  44968  etransclem35  44971  sge0reval  45074  sge0sn  45081  nnfoctbdjlem  45157  isomenndlem  45232  ovnn0val  45253  ovnsubaddlem1  45272  hoidmvn0val  45286  hsphoidmvle2  45287  hsphoidmvle  45288  hoidmvval0  45289  hoidmv1lelem2  45294  hoidmvlelem2  45298  hoidmvlelem3  45299  ovnhoilem1  45303  hspmbllem1  45328  hspmbllem2  45329  volico2  45343  ovolval2lem  45345  ovnsubadd2lem  45347  ovolval4lem1  45351  ovnovollem3  45360  vonioo  45384  vonicc  45387  prproropf1olem3  46159  fdmdifeqresdif  46970  dig1  47247  dignn0flhalflem1  47254  itcoval1  47302  itcoval2  47303  itcoval3  47304  itcovalsuc  47306  ackvalsuc1mpt  47317