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

Theorem iffalsed 4301
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 4299 . 2 𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐵)
31, 2syl 17 1 (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1637  ifcif 4290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-if 4291
This theorem is referenced by:  ifeqor  4339  ifnot  4340  ifan  4341  somincom  5755  mpt2difsnif  6993  tz7.44-2  7749  tz7.44-3  7750  unxpdomlem2  8414  sniffsupp  8564  unwdomg  8738  cantnfp1lem1  8832  cantnfp1lem3  8834  cantnflem1d  8842  updjudhcoinrg  9052  ttukeylem7  9632  canthp1lem2  9770  pwfseqlem3  9777  xmulneg1  12337  rexmul  12339  xmulpnf1  12342  fzprval  12644  expnnval  13106  expneg  13111  ccatval2  13595  ccatalpha  13610  swrdnd  13676  swrdnd2  13677  swrd0  13678  swrdccatin2  13731  relexpsucnnr  14008  relexp1g  14009  sgnp  14073  sgnn  14077  absmax  14312  sumss2  14700  fsumsplit  14714  fprodntriv  14913  fprodsplit  14937  ef0lem  15049  rpnnen2lem9  15191  sadadd2  15421  eucalgf  15535  eucalginv  15536  eucalglt  15537  iserodd  15777  pcmpt  15833  pcmpt2  15834  ramtub  15953  gsumval2a  17504  mgm2nsgrplem2  17631  mgm2nsgrplem3  17632  sgrp2nmndlem3  17637  mulgnn  17772  mulgnegnn  17776  symgextfv  18059  pmtrprfv3  18095  pmtrdifellem4  18120  pmtrprfval  18128  pmtrprfvalrn  18129  odlem2  18179  dfod2  18202  gsumval3a  18525  gsumzsplit  18548  dmdprdsplitlem  18658  abvtrivd  19064  psrlidm  19632  psrridm  19633  mvrcl  19678  mplmon  19692  mplmonmul  19693  mplcoe1  19694  mplcoe5  19697  evlslem3  19742  coe1tmfv2  19873  cply1coe0  19897  cply1coe0bi  19898  gsummoncoe1  19902  uvcvv0  20360  uvcff  20361  mulmarep1gsum1  20611  1marepvsma1  20621  mdetunilem2  20651  mdetunilem9  20658  maducoeval2  20678  symgmatr01lem  20692  gsummatr01lem3  20696  gsummatr01lem4  20697  gsummatr01  20698  m2cpm  20780  m2cpminvid2lem  20793  pmatcollpw3fi1lem1  20825  mp2pm2mplem4  20848  chfacffsupp  20895  chfacfscmul0  20897  chfacfpmmul0  20901  ptpjpre2  21618  ptopn2  21622  xkopt  21693  tsmssplit  22189  xrsxmet  22846  htpycc  23013  pco1  23048  pcohtpylem  23052  pcoass  23057  pcorevlem  23059  ovolunlem1a  23500  ovolunlem1  23501  ovolicc1  23520  itg11  23695  mbfi1flim  23727  itg2split  23753  itg2cnlem1  23765  itgeq2  23781  itgss2  23816  itgss3  23818  itgless  23820  ibladdlem  23823  itgaddlem1  23826  itggt0  23845  itgcn  23846  dvexp2  23954  lhop2  24015  deg1add  24100  ig1pval3  24171  ply1termlem  24196  plyeq0lem  24203  plypf1  24205  dvply1  24276  pserdvlem2  24419  abelthlem9  24431  logtayllem  24642  logtayl  24643  cxpef  24648  rlimcnp2  24930  efrlim  24933  muinv  25156  bposlem5  25250  lgsval2lem  25269  lgsval4  25279  lgsval4a  25281  lgsneg  25283  lgsneg1  25284  lgsdilem  25286  lgsdir  25294  lgsne0  25297  gausslemma2dlem1a  25327  gausslemma2dlem3  25330  2lgslem3  25366  rplogsumlem2  25411  dchrisum0fno1  25437  rplogsum  25453  pntrlog2bndlem4  25506  pntrlog2bndlem5  25507  padicabv  25556  ostth1  25559  ostth3  25564  axlowdim  26078  vtxval  26115  iedgval  26116  funvtxdmge2val  26128  funiedgdmge2val  26129  funvtxdm2val  26130  funiedgdm2val  26131  funvtxdm2valOLD  26132  funiedgdm2valOLD  26133  funvtxdmge2valOLD  26136  funiedgdmge2valOLD  26137  snstrvtxval  26166  snstriedgval  26167  crctcshwlkn0lem3  26956  crctcsh  26968  clwlkclwwlklem2fv2  27162  eucrct2eupth  27441  partfun  29825  psgnfzto1stlem  30198  pmtridfv1  30205  pmtridfv2  30206  smattr  30213  smatbl  30214  smatbr  30215  1smat1  30218  submatminr1  30224  madjusmdetlem1  30241  madjusmdetlem2  30242  xrge0iifcv  30328  xrge0iif1  30332  ind0  30428  esumpinfval  30483  sigaclfu2  30532  eulerpartlemgs2  30790  ballotlemrv2  30931  signswmnd  30982  signswlid  30984  signsvtp  31008  signlem0  31012  mrsubcn  31761  bcneg1  31966  bccolsum  31969  dfrdg2  32043  dfrdg4  32401  unblimceq0lem  32836  unbdqndv2lem2  32840  finxpreclem3  33565  finxpreclem5  33567  poimirlem1  33742  poimirlem2  33743  poimirlem7  33748  poimirlem10  33751  poimirlem11  33752  poimirlem16  33757  poimirlem17  33758  poimirlem20  33761  poimirlem24  33765  mblfinlem2  33779  itg2addnclem2  33793  ibladdnclem  33797  ftc1anclem6  33821  ftc1anclem8  33823  fdc  33871  heiborlem6  33945  cdleme31fv2  36192  cdlemefr27cl  36202  kelac1  38152  flcidc  38263  relexp01min  38523  relexpxpmin  38527  clsk1indlem0  38857  refsum2cnlem1  39708  upbdrech2  40021  ssfiunibd  40022  ioondisj2  40216  limsup10exlem  40502  icccncfext  40598  cncfiooicclem1  40604  cncfioobdlem  40607  dvnxpaek  40655  dvnprodlem1  40659  ditgeqiooicc  40673  iblcncfioo  40691  volioore  40704  dirkercncflem2  40818  dirkercncflem4  40820  fourierdlem40  40861  fourierdlem56  40876  fourierdlem65  40885  fourierdlem66  40886  fourierdlem73  40893  fourierdlem74  40894  fourierdlem75  40895  fourierdlem78  40898  fourierdlem79  40899  fourierdlem81  40901  fourierdlem82  40902  fourierdlem97  40917  fourierdlem103  40923  fourierdlem104  40924  sqwvfoura  40942  sqwvfourb  40943  fourierswlem  40944  fouriersw  40945  etransclem4  40952  etransclem14  40962  etransclem20  40968  etransclem22  40970  etransclem24  40972  etransclem25  40973  etransclem31  40979  etransclem32  40980  etransclem35  40983  sge0reval  41086  sge0sn  41093  nnfoctbdjlem  41169  isomenndlem  41244  ovnn0val  41265  ovnsubaddlem1  41284  hoidmvn0val  41298  hsphoidmvle2  41299  hsphoidmvle  41300  hoidmvval0  41301  hoidmv1lelem2  41306  hoidmvlelem2  41310  hoidmvlelem3  41311  ovnhoilem1  41315  hspmbllem1  41340  hspmbllem2  41341  volico2  41355  ovolval2lem  41357  ovnsubadd2lem  41359  ovolval4lem1  41363  ovnovollem3  41372  vonioo  41396  vonicc  41399  fdmdifeqresdif  42706  dig1  42988  dignn0flhalflem1  42995
  Copyright terms: Public domain W3C validator