MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iffalsed Structured version   Visualization version   GIF version

Theorem iffalsed 4502
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
StepHypRef Expression
1 iffalsed.1 . 2 (𝜑 → ¬ 𝜒)
2 iffalse 4500 . 2 𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐵)
31, 2syl 17 1 (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  ifcif 4491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-if 4492
This theorem is referenced by:  ifeqor  4542  ifnot  4543  ifan  4544  somincom  6093  partfun  6653  mpodifsnif  7476  tz7.44-2  8358  tz7.44-3  8359  unxpdomlem2  9202  sniffsupp  9343  unwdomg  9527  cantnfp1lem1  9621  cantnfp1lem3  9623  cantnflem1d  9631  ttrcltr  9659  updjudhcoinrg  9876  ttukeylem7  10458  canthp1lem2  10596  pwfseqlem3  10603  xmulneg1  13195  rexmul  13197  xmulpnf1  13200  fzprval  13509  expnnval  13977  expneg  13982  ccatval2  14473  ccatalpha  14488  swrdnd  14549  swrdnd2  14550  swrd0  14553  swrdccatin2  14624  relexpsucnnr  14917  relexp1g  14918  sgnp  14982  sgnn  14986  absmax  15221  sumss2  15618  fsumsplit  15633  fprodntriv  15832  fprodsplit  15856  ef0lem  15968  rpnnen2lem9  16111  sadadd2  16347  eucalgf  16466  eucalginv  16467  eucalglt  16468  iserodd  16714  pcmpt  16771  pcmpt2  16772  ramtub  16891  prmo1  16916  fvprif  17450  gsumval2a  18547  mgm2nsgrplem2  18736  mgm2nsgrplem3  18737  sgrp2nmndlem3  18742  mulgnn  18887  mulgnegnn  18893  symgextfv  19207  pmtrprfv3  19243  pmtrdifellem4  19268  pmtrprfval  19276  pmtrprfvalrn  19277  odlem2  19328  dfod2  19353  gsumval3a  19687  gsumzsplit  19711  dmdprdsplitlem  19823  ablsimpgfind  19896  abvtrivd  20315  uvcvv0  21212  uvcff  21213  psrlidm  21388  psrridm  21389  mvrcl  21437  mplmon  21452  mplmonmul  21453  mplcoe1  21454  mplcoe5  21457  evlslem3  21506  coe1tmfv2  21662  cply1coe0  21686  cply1coe0bi  21687  gsummoncoe1  21691  mulmarep1gsum1  21938  1marepvsma1  21948  mdetunilem2  21978  mdetunilem9  21985  maducoeval2  22005  symgmatr01lem  22018  gsummatr01lem3  22022  gsummatr01lem4  22023  gsummatr01  22024  m2cpm  22106  m2cpminvid2lem  22119  pmatcollpw3fi1lem1  22151  mp2pm2mplem4  22174  chfacffsupp  22221  chfacfscmul0  22223  chfacfpmmul0  22227  ptpjpre2  22947  ptopn2  22951  xkopt  23022  tsmssplit  23519  xrsxmet  24188  htpycc  24359  pco1  24394  pcohtpylem  24398  pcoass  24403  pcorevlem  24405  ovolunlem1a  24876  ovolunlem1  24877  ovolicc1  24896  itg11  25071  mbfi1flim  25104  itg2split  25130  itg2cnlem1  25142  itgeq2  25158  iblss  25185  itgss2  25193  itgss3  25195  itgless  25197  ibladdlem  25200  itgaddlem1  25203  itggt0  25224  itgcn  25225  dvexp2  25334  lhop2  25395  deg1add  25484  ig1pval3  25555  ply1termlem  25580  plyeq0lem  25587  plypf1  25589  dvply1  25660  pserdvlem2  25803  abelthlem9  25815  logtayllem  26030  logtayl  26031  cxpef  26036  rlimcnp2  26332  efrlim  26335  muinv  26558  bposlem5  26652  lgsval2lem  26671  lgsval4  26681  lgsval4a  26683  lgsneg  26685  lgsneg1  26686  lgsdilem  26688  lgsdir  26696  lgsne0  26699  gausslemma2dlem1a  26729  gausslemma2dlem3  26732  2lgslem3  26768  2sqnn0  26802  rplogsumlem2  26849  dchrisum0fno1  26875  rplogsum  26891  pntrlog2bndlem4  26944  pntrlog2bndlem5  26945  padicabv  26994  ostth1  26997  ostth3  27002  axlowdim  27952  vtxval  27993  iedgval  27994  funvtxdmge2val  28004  funiedgdmge2val  28005  funvtxdm2val  28006  funiedgdm2val  28007  snstrvtxval  28030  snstriedgval  28031  crctcshwlkn0lem3  28799  crctcsh  28811  clwlkclwwlklem2fv2  28982  eucrct2eupth  29231  pmtridfv1  31986  pmtridfv2  31987  psgnfzto1stlem  31991  smattr  32420  smatbl  32421  smatbr  32422  1smat1  32425  submatminr1  32431  madjusmdetlem1  32448  madjusmdetlem2  32449  xrge0iifcv  32555  xrge0iif1  32559  ind0  32657  esumpinfval  32712  sigaclfu2  32760  eulerpartlemgs2  33020  ballotlemrv2  33161  signswmnd  33209  signswlid  33211  signsvtp  33235  signlem0  33239  ex-sategoelelomsuc  34060  ex-sategoelel12  34061  mrsubcn  34153  bcneg1  34348  bccolsum  34351  dfrdg2  34409  dfrdg4  34565  unblimceq0lem  34998  unbdqndv2lem2  35002  finxpreclem3  35893  finxpreclem5  35895  poimirlem1  36108  poimirlem2  36109  poimirlem7  36114  poimirlem10  36117  poimirlem11  36118  poimirlem16  36123  poimirlem17  36124  poimirlem20  36127  poimirlem24  36131  mblfinlem2  36145  itg2addnclem2  36159  ibladdnclem  36163  ftc1anclem6  36185  ftc1anclem8  36187  fdc  36233  heiborlem6  36304  cdleme31fv2  38885  cdlemefr27cl  38895  sticksstones10  40592  sticksstones12a  40594  sticksstones12  40595  metakunt21  40626  metakunt27  40632  metakunt28  40633  metakunt29  40634  metakunt30  40635  metakunt31  40636  evlsbagval  40777  fsuppssind  40797  mhpind  40798  mhphf  40800  prjspner1  40993  kelac1  41419  flcidc  41530  oe0suclim  41641  oe0rif  41649  cantnfub  41685  cantnfresb  41688  sqrtcval  41987  relexp01min  42059  relexpxpmin  42063  clsk1indlem0  42387  refsum2cnlem1  43316  upbdrech2  43616  ssfiunibd  43617  ioondisj2  43805  limsup10exlem  44087  icccncfext  44202  cncfiooicclem1  44208  cncfioobdlem  44211  dvnxpaek  44257  dvnprodlem1  44261  ditgeqiooicc  44275  iblcncfioo  44293  volioore  44305  dirkercncflem2  44419  dirkercncflem4  44421  fourierdlem40  44462  fourierdlem56  44477  fourierdlem65  44486  fourierdlem66  44487  fourierdlem73  44494  fourierdlem74  44495  fourierdlem75  44496  fourierdlem78  44499  fourierdlem79  44500  fourierdlem81  44502  fourierdlem82  44503  fourierdlem97  44518  fourierdlem103  44524  fourierdlem104  44525  sqwvfoura  44543  sqwvfourb  44544  fourierswlem  44545  fouriersw  44546  etransclem4  44553  etransclem14  44563  etransclem20  44569  etransclem22  44571  etransclem24  44573  etransclem25  44574  etransclem31  44580  etransclem32  44581  etransclem35  44584  sge0reval  44687  sge0sn  44694  nnfoctbdjlem  44770  isomenndlem  44845  ovnn0val  44866  ovnsubaddlem1  44885  hoidmvn0val  44899  hsphoidmvle2  44900  hsphoidmvle  44901  hoidmvval0  44902  hoidmv1lelem2  44907  hoidmvlelem2  44911  hoidmvlelem3  44912  ovnhoilem1  44916  hspmbllem1  44941  hspmbllem2  44942  volico2  44956  ovolval2lem  44958  ovnsubadd2lem  44960  ovolval4lem1  44964  ovnovollem3  44973  vonioo  44997  vonicc  45000  prproropf1olem3  45771  fdmdifeqresdif  46491  dig1  46768  dignn0flhalflem1  46775  itcoval1  46823  itcoval2  46824  itcoval3  46825  itcovalsuc  46827  ackvalsuc1mpt  46838
  Copyright terms: Public domain W3C validator