Theorem iffalsed 4536

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526

This theorem is referenced by:  ifeqor  4577  ifnot  4578  ifan  4579  somincom  6154  partfun  6715  mpodifsnif  7548  tz7.44-2  8447  tz7.44-3  8448  unxpdomlem2  9287  sniffsupp  9440  unwdomg  9624  cantnfp1lem1  9718  cantnfp1lem3  9720  cantnflem1d  9728  ttrcltr  9756  updjudhcoinrg  9973  ttukeylem7  10555  canthp1lem2  10693  pwfseqlem3  10700  xmulneg1  13311  rexmul  13313  xmulpnf1  13316  fzprval  13625  expnnval  14105  expneg  14110  tpf1ofv1  14536  tpf1ofv2  14537  ccatval2  14616  ccatalpha  14631  swrdnd  14692  swrdnd2  14693  swrd0  14696  swrdccatin2  14767  relexpsucnnr  15064  relexp1g  15065  sgnp  15129  sgnn  15133  absmax  15368  sumss2  15762  fsumsplit  15777  fprodntriv  15978  fprodsplit  16002  ef0lem  16114  rpnnen2lem9  16258  sadadd2  16497  eucalgf  16620  eucalginv  16621  eucalglt  16622  iserodd  16873  pcmpt  16930  pcmpt2  16931  ramtub  17050  prmo1  17075  fvprif  17606  gsumval2a  18698  mgm2nsgrplem2  18932  mgm2nsgrplem3  18933  sgrp2nmndlem3  18938  mulgnn  19093  mulgnegnn  19102  symgextfv  19436  pmtrprfv3  19472  pmtrdifellem4  19497  pmtrprfval  19505  pmtrprfvalrn  19506  odlem2  19557  dfod2  19582  gsumval3a  19921  gsumzsplit  19945  dmdprdsplitlem  20057  ablsimpgfind  20130  abvtrivd  20833  uvcvv0  21810  uvcff  21811  psrlidm  21982  psrridm  21983  mvrcl  22012  mplmon  22053  mplmonmul  22054  mplcoe1  22055  mplcoe5  22058  evlslem3  22104  coe1tmfv2  22278  cply1coe0  22305  cply1coe0bi  22306  gsummoncoe1  22312  mulmarep1gsum1  22579  1marepvsma1  22589  mdetunilem2  22619  mdetunilem9  22626  maducoeval2  22646  symgmatr01lem  22659  gsummatr01lem3  22663  gsummatr01lem4  22664  gsummatr01  22665  m2cpm  22747  m2cpminvid2lem  22760  pmatcollpw3fi1lem1  22792  mp2pm2mplem4  22815  chfacffsupp  22862  chfacfscmul0  22864  chfacfpmmul0  22868  ptpjpre2  23588  ptopn2  23592  xkopt  23663  tsmssplit  24160  xrsxmet  24831  htpycc  25012  pco1  25048  pcohtpylem  25052  pcoass  25057  pcorevlem  25059  ovolunlem1a  25531  ovolunlem1  25532  ovolicc1  25551  itg11  25726  mbfi1flim  25758  itg2split  25784  itg2cnlem1  25796  itgeq2  25813  iblss  25840  itgss2  25848  itgss3  25850  itgless  25852  ibladdlem  25855  itgaddlem1  25858  itggt0  25879  itgcn  25880  dvexp2  25992  lhop2  26054  deg1add  26142  ig1pval3  26217  ply1termlem  26242  plyeq0lem  26249  plypf1  26251  dvply1  26325  pserdvlem2  26472  abelthlem9  26484  logtayllem  26701  logtayl  26702  cxpef  26707  rlimcnp2  27009  efrlim  27012  efrlimOLD  27013  muinv  27236  bposlem5  27332  lgsval2lem  27351  lgsval4  27361  lgsval4a  27363  lgsneg  27365  lgsneg1  27366  lgsdilem  27368  lgsdir  27376  lgsne0  27379  gausslemma2dlem1a  27409  gausslemma2dlem3  27412  2lgslem3  27448  2sqnn0  27482  rplogsumlem2  27529  dchrisum0fno1  27555  rplogsum  27571  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  padicabv  27674  ostth1  27677  ostth3  27682  expsnnval  28409  axlowdim  28976  vtxval  29017  iedgval  29018  funvtxdmge2val  29028  funiedgdmge2val  29029  funvtxdm2val  29030  funiedgdm2val  29031  snstrvtxval  29054  snstriedgval  29055  crctcshwlkn0lem3  29832  crctcsh  29844  clwlkclwwlklem2fv2  30015  eucrct2eupth  30264  fmptunsnop  32709  ind0  32843  ccatws1f1o  32936  pmtridfv1  33115  pmtridfv2  33116  psgnfzto1stlem  33120  elrgspnlem2  33247  elrgspnlem3  33248  elrgspnlem4  33249  elrspunsn  33457  gsummoncoe1fzo  33618  rtelextdg2lem  33767  2sqr3minply  33791  smattr  33798  smatbl  33799  smatbr  33800  1smat1  33803  submatminr1  33809  madjusmdetlem1  33826  madjusmdetlem2  33827  xrge0iifcv  33933  xrge0iif1  33937  esumpinfval  34074  sigaclfu2  34122  eulerpartlemgs2  34382  ballotlemrv2  34524  signswmnd  34572  signswlid  34574  signsvtp  34598  signlem0  34602  ex-sategoelelomsuc  35431  ex-sategoelel12  35432  mrsubcn  35524  bcneg1  35736  bccolsum  35739  dfrdg2  35796  dfrdg4  35952  unblimceq0lem  36507  unbdqndv2lem2  36511  finxpreclem3  37394  finxpreclem5  37396  poimirlem1  37628  poimirlem2  37629  poimirlem7  37634  poimirlem10  37637  poimirlem11  37638  poimirlem16  37643  poimirlem17  37644  poimirlem20  37647  poimirlem24  37651  mblfinlem2  37665  itg2addnclem2  37679  ibladdnclem  37683  ftc1anclem6  37705  ftc1anclem8  37707  fdc  37752  heiborlem6  37823  cdleme31fv2  40395  cdlemefr27cl  40405  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  metakunt21  42226  metakunt27  42232  metakunt28  42233  metakunt29  42234  metakunt30  42235  metakunt31  42236  evlsbagval  42576  selvvvval  42595  fsuppssind  42603  mhpind  42604  prjspner1  42636  kelac1  43075  flcidc  43182  oe0suclim  43290  oe0rif  43298  cantnfub  43334  cantnfresb  43337  tfsconcatfv  43354  sqrtcval  43654  relexp01min  43726  relexpxpmin  43730  clsk1indlem0  44054  refsum2cnlem1  45042  upbdrech2  45320  ssfiunibd  45321  ioondisj2  45506  limsup10exlem  45787  icccncfext  45902  cncfiooicclem1  45908  cncfioobdlem  45911  dvnxpaek  45957  dvnprodlem1  45961  ditgeqiooicc  45975  iblcncfioo  45993  volioore  46005  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem40  46162  fourierdlem56  46177  fourierdlem65  46186  fourierdlem66  46187  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem78  46199  fourierdlem79  46200  fourierdlem81  46202  fourierdlem82  46203  fourierdlem97  46218  fourierdlem103  46224  fourierdlem104  46225  sqwvfoura  46243  sqwvfourb  46244  fourierswlem  46245  fouriersw  46246  etransclem4  46253  etransclem14  46263  etransclem20  46269  etransclem22  46271  etransclem24  46273  etransclem25  46274  etransclem31  46280  etransclem32  46281  etransclem35  46284  sge0reval  46387  sge0sn  46394  nnfoctbdjlem  46470  isomenndlem  46545  ovnn0val  46566  ovnsubaddlem1  46585  hoidmvn0val  46599  hsphoidmvle2  46600  hsphoidmvle  46601  hoidmvval0  46602  hoidmv1lelem2  46607  hoidmvlelem2  46611  hoidmvlelem3  46612  ovnhoilem1  46616  hspmbllem1  46641  hspmbllem2  46642  volico2  46656  ovolval2lem  46658  ovnsubadd2lem  46660  ovolval4lem1  46664  ovnovollem3  46673  vonioo  46697  vonicc  46700  prproropf1olem3  47492  fdmdifeqresdif  48258  dig1  48529  dignn0flhalflem1  48536  itcoval1  48584  itcoval2  48585  itcoval3  48586  itcovalsuc  48588  ackvalsuc1mpt  48599