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

Theorem iffalsed 4046
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 4044 . 2 𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐵)
31, 2syl 17 1 (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  ifcif 4035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-if 4036
This theorem is referenced by:  ifeqor  4081  ifnot  4082  ifan  4083  somincom  5435  mpt2difsnif  6628  tz7.44-2  7367  tz7.44-3  7368  unxpdomlem2  8027  sniffsupp  8175  unwdomg  8349  cantnfp1lem1  8435  cantnfp1lem3  8437  cantnflem1d  8445  ttukeylem7  9197  canthp1lem2  9331  pwfseqlem3  9338  xmulneg1  11930  rexmul  11932  xmulpnf1  11935  fzprval  12228  expnnval  12682  expneg  12687  ccatval2  13163  ccatalpha  13176  swrdnd  13232  swrdnd2  13233  swrd0  13234  swrdccatin2  13286  relexpsucnnr  13561  relexp1g  13562  sgnp  13626  sgnn  13630  absmax  13865  sumss2  14252  fsumsplit  14266  fprodntriv  14459  fprodsplit  14483  ef0lem  14596  rpnnen2lem9  14738  sadadd2  14968  eucalgf  15082  eucalginv  15083  eucalglt  15084  iserodd  15326  pcmpt  15382  pcmpt2  15383  ramtub  15502  gsumval2a  17050  mgm2nsgrplem2  17177  mgm2nsgrplem3  17178  sgrp2nmndlem3  17183  mulgnn  17318  mulgnegnn  17322  symgextfv  17609  pmtrprfv3  17645  pmtrdifellem4  17670  pmtrprfval  17678  pmtrprfvalrn  17679  odlem2  17729  dfod2  17752  gsumval3a  18075  gsumzsplit  18098  dmdprdsplitlem  18207  abvtrivd  18611  psrlidm  19172  psrridm  19173  mvrcl  19218  mplmon  19232  mplmonmul  19233  mplcoe1  19234  mplcoe5  19237  evlslem3  19283  coe1tmfv2  19414  cply1coe0  19438  cply1coe0bi  19439  gsummoncoe1  19443  uvcvv0  19895  uvcff  19896  mulmarep1gsum1  20145  1marepvsma1  20155  mdetunilem2  20185  mdetunilem9  20192  maducoeval2  20212  symgmatr01lem  20225  gsummatr01lem3  20229  gsummatr01lem4  20230  gsummatr01  20231  m2cpm  20312  m2cpminvid2lem  20325  pmatcollpw3fi1lem1  20357  mp2pm2mplem4  20380  chfacffsupp  20427  chfacfscmul0  20429  chfacfpmmul0  20433  ptpjpre2  21140  ptopn2  21144  xkopt  21215  tsmssplit  21712  xrsxmet  22367  htpycc  22534  pco1  22570  pcohtpylem  22574  pcoass  22579  pcorevlem  22581  ovolunlem1a  23015  ovolunlem1  23016  ovolicc1  23035  itg11  23208  mbfi1flim  23240  itg2split  23266  itg2cnlem1  23278  itgeq2  23294  itgss2  23329  itgss3  23331  itgless  23333  ibladdlem  23336  itgaddlem1  23339  itggt0  23358  itgcn  23359  dvexp2  23467  lhop2  23526  deg1add  23611  ig1pval3  23682  ply1termlem  23707  plyeq0lem  23714  plypf1  23716  dvply1  23787  pserdvlem2  23930  abelthlem9  23942  logtayllem  24149  logtayl  24150  cxpef  24155  rlimcnp2  24437  efrlim  24440  muinv  24663  bposlem5  24757  lgsval2lem  24776  lgsval4  24786  lgsval4a  24788  lgsneg  24790  lgsneg1  24791  lgsdilem  24793  lgsdir  24801  lgsne0  24804  gausslemma2dlem1a  24834  gausslemma2dlem3  24837  2lgslem3  24873  rplogsumlem2  24918  dchrisum0fno1  24944  rplogsum  24960  pntrlog2bndlem4  25013  pntrlog2bndlem5  25014  padicabv  25063  ostth1  25066  ostth3  25071  axlowdim  25586  clwlkisclwwlklem2fv2  26104  partfun  28651  psgnfzto1stlem  28974  smattr  28986  smatbl  28987  smatbr  28988  1smat1  28991  submatminr1  28997  madjusmdetlem1  29014  madjusmdetlem2  29015  xrge0iifcv  29101  xrge0iif1  29105  ind0  29202  esumpinfval  29255  sigaclfu2  29304  eulerpartlemgs2  29562  ballotlemrv2  29703  signswmnd  29753  signswlid  29755  signsvtp  29779  signlem0  29783  mrsubcn  30463  bcneg1  30668  bccolsum  30671  dfrdg2  30738  dfrdg4  31021  unblimceq0lem  31460  unbdqndv2lem2  31464  finxpreclem3  32189  finxpreclem5  32191  poimirlem1  32363  poimirlem2  32364  poimirlem7  32369  poimirlem10  32372  poimirlem11  32373  poimirlem16  32378  poimirlem17  32379  poimirlem20  32382  poimirlem24  32386  mblfinlem2  32400  itg2addnclem2  32415  ibladdnclem  32419  ftc1anclem6  32443  ftc1anclem8  32445  fdc  32494  heiborlem6  32568  cdleme31fv2  34482  cdlemefr27cl  34492  kelac1  36434  flcidc  36546  relexp01min  36807  relexpxpmin  36811  clsk1indlem0  37142  refsum2cnlem1  38002  upbdrech2  38246  ssfiunibd  38247  ioondisj2  38344  icccncfext  38556  cncfiooicclem1  38562  cncfioobdlem  38565  dvnxpaek  38615  dvnprodlem1  38619  ditgeqiooicc  38635  iblcncfioo  38653  volioore  38666  dirkercncflem2  38780  dirkercncflem4  38782  fourierdlem40  38823  fourierdlem56  38838  fourierdlem65  38847  fourierdlem66  38848  fourierdlem73  38855  fourierdlem74  38856  fourierdlem75  38857  fourierdlem78  38860  fourierdlem79  38861  fourierdlem81  38863  fourierdlem82  38864  fourierdlem97  38879  fourierdlem103  38885  fourierdlem104  38886  sqwvfoura  38904  sqwvfourb  38905  fourierswlem  38906  fouriersw  38907  etransclem4  38914  etransclem14  38924  etransclem20  38930  etransclem22  38932  etransclem24  38934  etransclem25  38935  etransclem31  38941  etransclem32  38942  etransclem35  38945  sge0reval  39048  sge0sn  39055  nnfoctbdjlem  39131  isomenndlem  39203  ovnn0val  39224  ovnsubaddlem1  39243  hoidmvn0val  39257  hsphoidmvle2  39258  hsphoidmvle  39259  hoidmvval0  39260  hoidmv1lelem2  39265  hoidmvlelem2  39269  hoidmvlelem3  39270  ovnhoilem1  39274  hspmbllem1  39299  hspmbllem2  39300  volico2  39314  ovolval2lem  39316  ovnsubadd2lem  39318  ovolval4lem1  39322  ovnovollem3  39331  vonioo  39356  vonicc  39359  funvtxdm2val  40225  funiedgdm2val  40226  funvtxdmge2val  40228  funiedgdmge2val  40229  snstrvtxval  40249  snstriedgval  40250  crctcsh1wlkn0lem3  40996  crctcsh  41008  clwlkclwwlklem2fv2  41186  eucrct2eupth  41394  fdmdifeqresdif  41894  dig1  42181  dignn0flhalflem1  42188
  Copyright terms: Public domain W3C validator