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

Theorem iffalsed 4476
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 4474 . 2 𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐵)
31, 2syl 17 1 (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  ifcif 4465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-ex 1772  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4466
This theorem is referenced by:  ifeqor  4514  ifnot  4515  ifan  4516  somincom  5988  mpodifsnif  7256  tz7.44-2  8034  tz7.44-3  8035  unxpdomlem2  8712  sniffsupp  8862  unwdomg  9037  cantnfp1lem1  9130  cantnfp1lem3  9132  cantnflem1d  9140  updjudhcoinrg  9351  ttukeylem7  9926  canthp1lem2  10064  pwfseqlem3  10071  xmulneg1  12652  rexmul  12654  xmulpnf1  12657  fzprval  12958  expnnval  13422  expneg  13427  ccatval2  13922  ccatalpha  13937  swrdnd  14006  swrdnd2  14007  swrd0  14010  swrdccatin2  14081  relexpsucnnr  14374  relexp1g  14375  sgnp  14439  sgnn  14443  absmax  14679  sumss2  15073  fsumsplit  15087  fprodntriv  15286  fprodsplit  15310  ef0lem  15422  rpnnen2lem9  15565  sadadd2  15799  eucalgf  15917  eucalginv  15918  eucalglt  15919  iserodd  16162  pcmpt  16218  pcmpt2  16219  ramtub  16338  prmo1  16363  fvprif  16824  gsumval2a  17885  mgm2nsgrplem2  18024  mgm2nsgrplem3  18025  sgrp2nmndlem3  18030  mulgnn  18172  mulgnegnn  18178  symgextfv  18477  pmtrprfv3  18513  pmtrdifellem4  18538  pmtrprfval  18546  pmtrprfvalrn  18547  odlem2  18598  dfod2  18622  gsumval3a  18954  gsumzsplit  18978  dmdprdsplitlem  19090  ablsimpgfind  19163  abvtrivd  19542  psrlidm  20113  psrridm  20114  mvrcl  20159  mplmon  20174  mplmonmul  20175  mplcoe1  20176  mplcoe5  20179  evlslem3  20223  coe1tmfv2  20373  cply1coe0  20397  cply1coe0bi  20398  gsummoncoe1  20402  uvcvv0  20864  uvcff  20865  mulmarep1gsum1  21112  1marepvsma1  21122  mdetunilem2  21152  mdetunilem9  21159  maducoeval2  21179  symgmatr01lem  21192  gsummatr01lem3  21196  gsummatr01lem4  21197  gsummatr01  21198  m2cpm  21279  m2cpminvid2lem  21292  pmatcollpw3fi1lem1  21324  mp2pm2mplem4  21347  chfacffsupp  21394  chfacfscmul0  21396  chfacfpmmul0  21400  ptpjpre2  22118  ptopn2  22122  xkopt  22193  tsmssplit  22689  xrsxmet  23346  htpycc  23513  pco1  23548  pcohtpylem  23552  pcoass  23557  pcorevlem  23559  ovolunlem1a  24026  ovolunlem1  24027  ovolicc1  24046  itg11  24221  mbfi1flim  24253  itg2split  24279  itg2cnlem1  24291  itgeq2  24307  iblss  24334  itgss2  24342  itgss3  24344  itgless  24346  ibladdlem  24349  itgaddlem1  24352  itggt0  24371  itgcn  24372  dvexp2  24480  lhop2  24541  deg1add  24626  ig1pval3  24697  ply1termlem  24722  plyeq0lem  24729  plypf1  24731  dvply1  24802  pserdvlem2  24945  abelthlem9  24957  logtayllem  25169  logtayl  25170  cxpef  25175  rlimcnp2  25472  efrlim  25475  muinv  25698  bposlem5  25792  lgsval2lem  25811  lgsval4  25821  lgsval4a  25823  lgsneg  25825  lgsneg1  25826  lgsdilem  25828  lgsdir  25836  lgsne0  25839  gausslemma2dlem1a  25869  gausslemma2dlem3  25872  2lgslem3  25908  2sqnn0  25942  rplogsumlem2  25989  dchrisum0fno1  26015  rplogsum  26031  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  padicabv  26134  ostth1  26137  ostth3  26142  axlowdim  26675  vtxval  26713  iedgval  26714  funvtxdmge2val  26724  funiedgdmge2val  26725  funvtxdm2val  26726  funiedgdm2val  26727  snstrvtxval  26750  snstriedgval  26751  crctcshwlkn0lem3  27518  crctcsh  27530  clwlkclwwlklem2fv2  27702  eucrct2eupth  27952  partfun  30350  pmtridfv1  30665  pmtridfv2  30666  psgnfzto1stlem  30670  smattr  30964  smatbl  30965  smatbr  30966  1smat1  30969  submatminr1  30975  madjusmdetlem1  30992  madjusmdetlem2  30993  xrge0iifcv  31077  xrge0iif1  31081  ind0  31177  esumpinfval  31232  sigaclfu2  31280  eulerpartlemgs2  31538  ballotlemrv2  31679  signswmnd  31727  signswlid  31729  signsvtp  31753  signlem0  31757  ex-sategoelelomsuc  32571  ex-sategoelel12  32572  mrsubcn  32664  bcneg1  32866  bccolsum  32869  dfrdg2  32938  dfrdg4  33310  unblimceq0lem  33743  unbdqndv2lem2  33747  finxpreclem3  34557  finxpreclem5  34559  poimirlem1  34775  poimirlem2  34776  poimirlem7  34781  poimirlem10  34784  poimirlem11  34785  poimirlem16  34790  poimirlem17  34791  poimirlem20  34794  poimirlem24  34798  mblfinlem2  34812  itg2addnclem2  34826  ibladdnclem  34830  ftc1anclem6  34854  ftc1anclem8  34856  fdc  34903  heiborlem6  34977  cdleme31fv2  37411  cdlemefr27cl  37421  kelac1  39543  flcidc  39654  relexp01min  39938  relexpxpmin  39942  clsk1indlem0  40271  refsum2cnlem1  41174  upbdrech2  41455  ssfiunibd  41456  ioondisj2  41647  limsup10exlem  41933  icccncfext  42050  cncfiooicclem1  42056  cncfioobdlem  42059  dvnxpaek  42107  dvnprodlem1  42111  ditgeqiooicc  42125  iblcncfioo  42143  volioore  42156  dirkercncflem2  42270  dirkercncflem4  42272  fourierdlem40  42313  fourierdlem56  42328  fourierdlem65  42337  fourierdlem66  42338  fourierdlem73  42345  fourierdlem74  42346  fourierdlem75  42347  fourierdlem78  42350  fourierdlem79  42351  fourierdlem81  42353  fourierdlem82  42354  fourierdlem97  42369  fourierdlem103  42375  fourierdlem104  42376  sqwvfoura  42394  sqwvfourb  42395  fourierswlem  42396  fouriersw  42397  etransclem4  42404  etransclem14  42414  etransclem20  42420  etransclem22  42422  etransclem24  42424  etransclem25  42425  etransclem31  42431  etransclem32  42432  etransclem35  42435  sge0reval  42535  sge0sn  42542  nnfoctbdjlem  42618  isomenndlem  42693  ovnn0val  42714  ovnsubaddlem1  42733  hoidmvn0val  42747  hsphoidmvle2  42748  hsphoidmvle  42749  hoidmvval0  42750  hoidmv1lelem2  42755  hoidmvlelem2  42759  hoidmvlelem3  42760  ovnhoilem1  42764  hspmbllem1  42789  hspmbllem2  42790  volico2  42804  ovolval2lem  42806  ovnsubadd2lem  42808  ovolval4lem1  42812  ovnovollem3  42821  vonioo  42845  vonicc  42848  prproropf1olem3  43514  fdmdifeqresdif  44288  dig1  44566  dignn0flhalflem1  44573
  Copyright terms: Public domain W3C validator