Theorem iffalsed 4472

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547  ifcif 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-if 4462

This theorem is referenced by:  ifeqor  4513  ifnot  4514  ifan  4515  somincom  6091  partfun  6639  mpodifsnif  7478  tz7.44-2  8343  tz7.44-3  8344  unxpdomlem2  9164  sniffsupp  9310  unwdomg  9496  cantnfp1lem1  9597  cantnfp1lem3  9599  cantnflem1d  9607  ttrcltr  9635  updjudhcoinrg  9855  ttukeylem7  10435  canthp1lem2  10574  pwfseqlem3  10581  ind0  12167  xmulneg1  13219  rexmul  13221  xmulpnf1  13224  fzprval  13537  expnnval  14024  expneg  14029  tpf1ofv1  14457  tpf1ofv2  14458  ccatval2  14538  ccatalpha  14554  swrdnd  14615  swrdnd2  14616  swrd0  14619  swrdccatin2  14689  relexpsucnnr  14985  relexp1g  14986  sgnp  15050  sgnn  15054  absmax  15290  sumss2  15686  fsumsplit  15701  fprodntriv  15905  fprodsplit  15929  ef0lem  16041  rpnnen2lem9  16187  sadadd2  16427  eucalgf  16550  eucalginv  16551  eucalglt  16552  iserodd  16804  pcmpt  16861  pcmpt2  16862  ramtub  16981  prmo1  17006  fvprif  17523  gsumval2a  18651  mgm2nsgrplem2  18888  mgm2nsgrplem3  18889  sgrp2nmndlem3  18894  mulgnn  19049  mulgnegnn  19058  symgextfv  19391  pmtrprfv3  19427  pmtrdifellem4  19452  pmtrprfval  19460  pmtrprfvalrn  19461  odlem2  19512  dfod2  19537  gsumval3a  19876  gsumzsplit  19900  dmdprdsplitlem  20012  ablsimpgfind  20085  abvtrivd  20811  uvcvv0  21772  uvcff  21773  psrlidm  21943  psrridm  21944  mvrcl  21973  mplmon  22018  mplmonmul  22019  mplcoe1  22020  mplcoe5  22023  evlslem3  22063  selvvvval  22125  coe1tmfv2  22268  cply1coe0  22294  cply1coe0bi  22295  gsummoncoe1  22301  mulmarep1gsum1  22563  1marepvsma1  22573  mdetunilem2  22603  mdetunilem9  22610  maducoeval2  22630  symgmatr01lem  22643  gsummatr01lem3  22647  gsummatr01lem4  22648  gsummatr01  22649  m2cpm  22731  m2cpminvid2lem  22744  pmatcollpw3fi1lem1  22776  mp2pm2mplem4  22799  chfacffsupp  22846  chfacfscmul0  22848  chfacfpmmul0  22852  ptpjpre2  23570  ptopn2  23574  xkopt  23645  tsmssplit  24142  xrsxmet  24800  htpycc  24972  pco1  25007  pcohtpylem  25011  pcoass  25016  pcorevlem  25018  ovolunlem1a  25488  ovolunlem1  25489  ovolicc1  25508  itg11  25683  mbfi1flim  25715  itg2split  25741  itg2cnlem1  25753  itgeq2  25770  iblss  25797  itgss2  25805  itgss3  25807  itgless  25809  ibladdlem  25812  itgaddlem1  25815  itggt0  25836  itgcn  25837  dvexp2  25946  lhop2  26007  deg1add  26093  ig1pval3  26168  ply1termlem  26193  plyeq0lem  26200  plypf1  26202  dvply1  26275  pserdvlem2  26418  abelthlem9  26430  logtayllem  26648  logtayl  26649  cxpef  26654  rlimcnp2  26955  efrlim  26958  muinv  27181  bposlem5  27276  lgsval2lem  27295  lgsval4  27305  lgsval4a  27307  lgsneg  27309  lgsneg1  27310  lgsdilem  27312  lgsdir  27320  lgsne0  27323  gausslemma2dlem1a  27353  gausslemma2dlem3  27356  2lgslem3  27392  2sqnn0  27426  rplogsumlem2  27473  dchrisum0fno1  27499  rplogsum  27515  pntrlog2bndlem4  27568  pntrlog2bndlem5  27569  padicabv  27618  ostth1  27621  ostth3  27626  expnnsval  28443  axlowdim  29055  vtxval  29094  iedgval  29095  funvtxdmge2val  29105  funiedgdmge2val  29106  funvtxdm2val  29107  funiedgdm2val  29108  snstrvtxval  29131  snstriedgval  29132  crctcshwlkn0lem3  29905  crctcsh  29917  clwlkclwwlklem2fv2  30091  eucrct2eupth  30340  fmptunsnop  32799  ccatws1f1o  33037  pmtridfv1  33183  pmtridfv2  33184  psgnfzto1stlem  33188  elrgspnlem2  33331  elrgspnlem3  33332  elrgspnlem4  33333  elrspunsn  33519  gsummoncoe1fzo  33687  mplasclco  33707  mplmulmvr  33730  evlextv  33733  psrmonmul  33741  esplyfval3  33763  esplyfval1  33764  esplyind  33766  extdgfialglem2  33884  rtelextdg2lem  33917  2sqr3minply  33971  cos9thpiminply  33979  smattr  33990  smatbl  33991  smatbr  33992  1smat1  33995  submatminr1  34001  madjusmdetlem1  34018  madjusmdetlem2  34019  xrge0iifcv  34125  xrge0iif1  34129  esumpinfval  34264  sigaclfu2  34312  eulerpartlemgs2  34571  ballotlemrv2  34713  signswmnd  34748  signswlid  34750  signsvtp  34774  signlem0  34778  ex-sategoelelomsuc  35661  ex-sategoelel12  35662  mrsubcn  35754  bcneg1  35971  bccolsum  35974  dfrdg2  36028  dfrdg4  36186  unblimceq0lem  36819  unbdqndv2lem2  36823  finxpreclem3  37762  finxpreclem5  37764  poimirlem1  37995  poimirlem2  37996  poimirlem7  38001  poimirlem10  38004  poimirlem11  38005  poimirlem16  38010  poimirlem17  38011  poimirlem20  38014  poimirlem24  38018  mblfinlem2  38032  itg2addnclem2  38046  ibladdnclem  38050  ftc1anclem6  38072  ftc1anclem8  38074  fdc  38119  heiborlem6  38190  cdleme31fv2  40892  cdlemefr27cl  40902  sticksstones10  42647  sticksstones12a  42649  sticksstones12  42650  evlsbagval  43043  fsuppssind  43050  mhpind  43051  prjspner1  43083  kelac1  43515  flcidc  43622  oe0suclim  43729  oe0rif  43737  cantnfub  43773  cantnfresb  43776  tfsconcatfv  43793  sqrtcval  44092  relexp01min  44164  relexpxpmin  44168  clsk1indlem0  44492  refsum2cnlem1  45492  upbdrech2  45763  ssfiunibd  45764  ioondisj2  45945  limsup10exlem  46222  icccncfext  46337  cncfiooicclem1  46343  cncfioobdlem  46346  dvnxpaek  46392  dvnprodlem1  46396  ditgeqiooicc  46410  iblcncfioo  46428  volioore  46440  dirkercncflem2  46554  dirkercncflem4  46556  fourierdlem40  46597  fourierdlem56  46612  fourierdlem65  46621  fourierdlem66  46622  fourierdlem73  46629  fourierdlem74  46630  fourierdlem75  46631  fourierdlem78  46634  fourierdlem79  46635  fourierdlem81  46637  fourierdlem82  46638  fourierdlem97  46653  fourierdlem103  46659  fourierdlem104  46660  sqwvfoura  46678  sqwvfourb  46679  fourierswlem  46680  fouriersw  46681  etransclem4  46688  etransclem14  46698  etransclem20  46704  etransclem22  46706  etransclem24  46708  etransclem25  46709  etransclem31  46715  etransclem32  46716  etransclem35  46719  sge0reval  46822  sge0sn  46829  nnfoctbdjlem  46905  isomenndlem  46980  ovnn0val  47001  ovnsubaddlem1  47020  hoidmvn0val  47034  hsphoidmvle2  47035  hsphoidmvle  47036  hoidmvval0  47037  hoidmv1lelem2  47042  hoidmvlelem2  47046  hoidmvlelem3  47047  ovnhoilem1  47051  hspmbllem1  47076  hspmbllem2  47077  volico2  47091  ovolval2lem  47093  ovnsubadd2lem  47095  ovolval4lem1  47099  ovnovollem3  47108  vonioo  47132  vonicc  47135  prproropf1olem3  47987  fdmdifeqresdif  48840  dig1  49106  dignn0flhalflem1  49113  itcoval1  49161  itcoval2  49162  itcoval3  49163  itcovalsuc  49165  ackvalsuc1mpt  49176