Theorem iffalsed 4499

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

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

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 4489

This theorem is referenced by:  ifeqor  4540  ifnot  4541  ifan  4542  somincom  6107  partfun  6665  mpodifsnif  7504  tz7.44-2  8375  tz7.44-3  8376  unxpdomlem2  9198  sniffsupp  9351  unwdomg  9537  cantnfp1lem1  9631  cantnfp1lem3  9633  cantnflem1d  9641  ttrcltr  9669  updjudhcoinrg  9886  ttukeylem7  10468  canthp1lem2  10606  pwfseqlem3  10613  xmulneg1  13229  rexmul  13231  xmulpnf1  13234  fzprval  13546  expnnval  14029  expneg  14034  tpf1ofv1  14462  tpf1ofv2  14463  ccatval2  14543  ccatalpha  14558  swrdnd  14619  swrdnd2  14620  swrd0  14623  swrdccatin2  14694  relexpsucnnr  14991  relexp1g  14992  sgnp  15056  sgnn  15060  absmax  15296  sumss2  15692  fsumsplit  15707  fprodntriv  15908  fprodsplit  15932  ef0lem  16044  rpnnen2lem9  16190  sadadd2  16430  eucalgf  16553  eucalginv  16554  eucalglt  16555  iserodd  16806  pcmpt  16863  pcmpt2  16864  ramtub  16983  prmo1  17008  fvprif  17524  gsumval2a  18612  mgm2nsgrplem2  18846  mgm2nsgrplem3  18847  sgrp2nmndlem3  18852  mulgnn  19007  mulgnegnn  19016  symgextfv  19348  pmtrprfv3  19384  pmtrdifellem4  19409  pmtrprfval  19417  pmtrprfvalrn  19418  odlem2  19469  dfod2  19494  gsumval3a  19833  gsumzsplit  19857  dmdprdsplitlem  19969  ablsimpgfind  20042  abvtrivd  20741  uvcvv0  21699  uvcff  21700  psrlidm  21871  psrridm  21872  mvrcl  21901  mplmon  21942  mplmonmul  21943  mplcoe1  21944  mplcoe5  21947  evlslem3  21987  coe1tmfv2  22161  cply1coe0  22188  cply1coe0bi  22189  gsummoncoe1  22195  mulmarep1gsum1  22460  1marepvsma1  22470  mdetunilem2  22500  mdetunilem9  22507  maducoeval2  22527  symgmatr01lem  22540  gsummatr01lem3  22544  gsummatr01lem4  22545  gsummatr01  22546  m2cpm  22628  m2cpminvid2lem  22641  pmatcollpw3fi1lem1  22673  mp2pm2mplem4  22696  chfacffsupp  22743  chfacfscmul0  22745  chfacfpmmul0  22749  ptpjpre2  23467  ptopn2  23471  xkopt  23542  tsmssplit  24039  xrsxmet  24698  htpycc  24879  pco1  24915  pcohtpylem  24919  pcoass  24924  pcorevlem  24926  ovolunlem1a  25397  ovolunlem1  25398  ovolicc1  25417  itg11  25592  mbfi1flim  25624  itg2split  25650  itg2cnlem1  25662  itgeq2  25679  iblss  25706  itgss2  25714  itgss3  25716  itgless  25718  ibladdlem  25721  itgaddlem1  25724  itggt0  25745  itgcn  25746  dvexp2  25858  lhop2  25920  deg1add  26008  ig1pval3  26083  ply1termlem  26108  plyeq0lem  26115  plypf1  26117  dvply1  26191  pserdvlem2  26338  abelthlem9  26350  logtayllem  26568  logtayl  26569  cxpef  26574  rlimcnp2  26876  efrlim  26879  efrlimOLD  26880  muinv  27103  bposlem5  27199  lgsval2lem  27218  lgsval4  27228  lgsval4a  27230  lgsneg  27232  lgsneg1  27233  lgsdilem  27235  lgsdir  27243  lgsne0  27246  gausslemma2dlem1a  27276  gausslemma2dlem3  27279  2lgslem3  27315  2sqnn0  27349  rplogsumlem2  27396  dchrisum0fno1  27422  rplogsum  27438  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  padicabv  27541  ostth1  27544  ostth3  27549  expsnnval  28312  axlowdim  28888  vtxval  28927  iedgval  28928  funvtxdmge2val  28938  funiedgdmge2val  28939  funvtxdm2val  28940  funiedgdm2val  28941  snstrvtxval  28964  snstriedgval  28965  crctcshwlkn0lem3  29742  crctcsh  29754  clwlkclwwlklem2fv2  29925  eucrct2eupth  30174  fmptunsnop  32623  ind0  32781  ccatws1f1o  32873  pmtridfv1  33052  pmtridfv2  33053  psgnfzto1stlem  33057  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnlem4  33196  elrspunsn  33400  gsummoncoe1fzo  33563  rtelextdg2lem  33716  2sqr3minply  33770  cos9thpiminply  33778  smattr  33789  smatbl  33790  smatbr  33791  1smat1  33794  submatminr1  33800  madjusmdetlem1  33817  madjusmdetlem2  33818  xrge0iifcv  33924  xrge0iif1  33928  esumpinfval  34063  sigaclfu2  34111  eulerpartlemgs2  34371  ballotlemrv2  34513  signswmnd  34548  signswlid  34550  signsvtp  34574  signlem0  34578  ex-sategoelelomsuc  35413  ex-sategoelel12  35414  mrsubcn  35506  bcneg1  35723  bccolsum  35726  dfrdg2  35783  dfrdg4  35939  unblimceq0lem  36494  unbdqndv2lem2  36498  finxpreclem3  37381  finxpreclem5  37383  poimirlem1  37615  poimirlem2  37616  poimirlem7  37621  poimirlem10  37624  poimirlem11  37625  poimirlem16  37630  poimirlem17  37631  poimirlem20  37634  poimirlem24  37638  mblfinlem2  37652  itg2addnclem2  37666  ibladdnclem  37670  ftc1anclem6  37692  ftc1anclem8  37694  fdc  37739  heiborlem6  37810  cdleme31fv2  40387  cdlemefr27cl  40397  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  evlsbagval  42554  selvvvval  42573  fsuppssind  42581  mhpind  42582  prjspner1  42614  kelac1  43052  flcidc  43159  oe0suclim  43266  oe0rif  43274  cantnfub  43310  cantnfresb  43313  tfsconcatfv  43330  sqrtcval  43630  relexp01min  43702  relexpxpmin  43706  clsk1indlem0  44030  refsum2cnlem1  45031  upbdrech2  45306  ssfiunibd  45307  ioondisj2  45491  limsup10exlem  45770  icccncfext  45885  cncfiooicclem1  45891  cncfioobdlem  45894  dvnxpaek  45940  dvnprodlem1  45944  ditgeqiooicc  45958  iblcncfioo  45976  volioore  45988  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem40  46145  fourierdlem56  46160  fourierdlem65  46169  fourierdlem66  46170  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem78  46182  fourierdlem79  46183  fourierdlem81  46185  fourierdlem82  46186  fourierdlem97  46201  fourierdlem103  46207  fourierdlem104  46208  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  etransclem4  46236  etransclem14  46246  etransclem20  46252  etransclem22  46254  etransclem24  46256  etransclem25  46257  etransclem31  46263  etransclem32  46264  etransclem35  46267  sge0reval  46370  sge0sn  46377  nnfoctbdjlem  46453  isomenndlem  46528  ovnn0val  46549  ovnsubaddlem1  46568  hoidmvn0val  46582  hsphoidmvle2  46583  hsphoidmvle  46584  hoidmvval0  46585  hoidmv1lelem2  46590  hoidmvlelem2  46594  hoidmvlelem3  46595  ovnhoilem1  46599  hspmbllem1  46624  hspmbllem2  46625  volico2  46639  ovolval2lem  46641  ovnsubadd2lem  46643  ovolval4lem1  46647  ovnovollem3  46656  vonioo  46680  vonicc  46683  prproropf1olem3  47506  fdmdifeqresdif  48330  dig1  48597  dignn0flhalflem1  48604  itcoval1  48652  itcoval2  48653  itcoval3  48654  itcovalsuc  48656  ackvalsuc1mpt  48667