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

Theorem iffalsed 4130
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 4128 . 2 𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐵)
31, 2syl 17 1 (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  ifcif 4119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-if 4120
This theorem is referenced by:  ifeqor  4165  ifnot  4166  ifan  4167  somincom  5565  mpt2difsnif  6795  tz7.44-2  7548  tz7.44-3  7549  unxpdomlem2  8206  sniffsupp  8356  unwdomg  8530  cantnfp1lem1  8613  cantnfp1lem3  8615  cantnflem1d  8623  ttukeylem7  9375  canthp1lem2  9513  pwfseqlem3  9520  xmulneg1  12137  rexmul  12139  xmulpnf1  12142  fzprval  12439  expnnval  12903  expneg  12908  ccatval2  13396  ccatalpha  13411  swrdnd  13478  swrdnd2  13479  swrd0  13480  swrdccatin2  13533  relexpsucnnr  13809  relexp1g  13810  sgnp  13874  sgnn  13878  absmax  14113  sumss2  14501  fsumsplit  14515  fprodntriv  14716  fprodsplit  14740  ef0lem  14853  rpnnen2lem9  14995  sadadd2  15229  eucalgf  15343  eucalginv  15344  eucalglt  15345  iserodd  15587  pcmpt  15643  pcmpt2  15644  ramtub  15763  gsumval2a  17326  mgm2nsgrplem2  17453  mgm2nsgrplem3  17454  sgrp2nmndlem3  17459  mulgnn  17594  mulgnegnn  17598  symgextfv  17884  pmtrprfv3  17920  pmtrdifellem4  17945  pmtrprfval  17953  pmtrprfvalrn  17954  odlem2  18004  dfod2  18027  gsumval3a  18350  gsumzsplit  18373  dmdprdsplitlem  18482  abvtrivd  18888  psrlidm  19451  psrridm  19452  mvrcl  19497  mplmon  19511  mplmonmul  19512  mplcoe1  19513  mplcoe5  19516  evlslem3  19562  coe1tmfv2  19693  cply1coe0  19717  cply1coe0bi  19718  gsummoncoe1  19722  uvcvv0  20177  uvcff  20178  mulmarep1gsum1  20427  1marepvsma1  20437  mdetunilem2  20467  mdetunilem9  20474  maducoeval2  20494  symgmatr01lem  20507  gsummatr01lem3  20511  gsummatr01lem4  20512  gsummatr01  20513  m2cpm  20594  m2cpminvid2lem  20607  pmatcollpw3fi1lem1  20639  mp2pm2mplem4  20662  chfacffsupp  20709  chfacfscmul0  20711  chfacfpmmul0  20715  ptpjpre2  21431  ptopn2  21435  xkopt  21506  tsmssplit  22002  xrsxmet  22659  htpycc  22826  pco1  22861  pcohtpylem  22865  pcoass  22870  pcorevlem  22872  ovolunlem1a  23310  ovolunlem1  23311  ovolicc1  23330  itg11  23503  mbfi1flim  23535  itg2split  23561  itg2cnlem1  23573  itgeq2  23589  itgss2  23624  itgss3  23626  itgless  23628  ibladdlem  23631  itgaddlem1  23634  itggt0  23653  itgcn  23654  dvexp2  23762  lhop2  23823  deg1add  23908  ig1pval3  23979  ply1termlem  24004  plyeq0lem  24011  plypf1  24013  dvply1  24084  pserdvlem2  24227  abelthlem9  24239  logtayllem  24450  logtayl  24451  cxpef  24456  rlimcnp2  24738  efrlim  24741  muinv  24964  bposlem5  25058  lgsval2lem  25077  lgsval4  25087  lgsval4a  25089  lgsneg  25091  lgsneg1  25092  lgsdilem  25094  lgsdir  25102  lgsne0  25105  gausslemma2dlem1a  25135  gausslemma2dlem3  25138  2lgslem3  25174  rplogsumlem2  25219  dchrisum0fno1  25245  rplogsum  25261  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  padicabv  25364  ostth1  25367  ostth3  25372  axlowdim  25886  vtxval  25923  iedgval  25924  funvtxdmge2val  25936  funiedgdmge2val  25937  funvtxdm2val  25938  funiedgdm2val  25939  funvtxdm2valOLD  25940  funiedgdm2valOLD  25941  funvtxdmge2valOLD  25944  funiedgdmge2valOLD  25945  snstrvtxval  25974  snstriedgval  25975  crctcshwlkn0lem3  26760  crctcsh  26772  clwlkclwwlklem2fv2  26962  eucrct2eupth  27223  partfun  29603  psgnfzto1stlem  29978  pmtridfv1  29985  pmtridfv2  29986  smattr  29993  smatbl  29994  smatbr  29995  1smat1  29998  submatminr1  30004  madjusmdetlem1  30021  madjusmdetlem2  30022  xrge0iifcv  30108  xrge0iif1  30112  ind0  30208  esumpinfval  30263  sigaclfu2  30312  eulerpartlemgs2  30570  ballotlemrv2  30711  signswmnd  30762  signswlid  30764  signsvtp  30788  signlem0  30792  mrsubcn  31542  bcneg1  31748  bccolsum  31751  dfrdg2  31825  dfrdg4  32183  unblimceq0lem  32622  unbdqndv2lem2  32626  finxpreclem3  33360  finxpreclem5  33362  poimirlem1  33540  poimirlem2  33541  poimirlem7  33546  poimirlem10  33549  poimirlem11  33550  poimirlem16  33555  poimirlem17  33556  poimirlem20  33559  poimirlem24  33563  mblfinlem2  33577  itg2addnclem2  33592  ibladdnclem  33596  ftc1anclem6  33620  ftc1anclem8  33622  fdc  33671  heiborlem6  33745  cdleme31fv2  35998  cdlemefr27cl  36008  kelac1  37950  flcidc  38061  relexp01min  38322  relexpxpmin  38326  clsk1indlem0  38656  refsum2cnlem1  39510  upbdrech2  39836  ssfiunibd  39837  ioondisj2  40032  limsup10exlem  40322  icccncfext  40418  cncfiooicclem1  40424  cncfioobdlem  40427  dvnxpaek  40475  dvnprodlem1  40479  ditgeqiooicc  40494  iblcncfioo  40512  volioore  40525  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem40  40682  fourierdlem56  40697  fourierdlem65  40706  fourierdlem66  40707  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem78  40719  fourierdlem79  40720  fourierdlem81  40722  fourierdlem82  40723  fourierdlem97  40738  fourierdlem103  40744  fourierdlem104  40745  sqwvfoura  40763  sqwvfourb  40764  fourierswlem  40765  fouriersw  40766  etransclem4  40773  etransclem14  40783  etransclem20  40789  etransclem22  40791  etransclem24  40793  etransclem25  40794  etransclem31  40800  etransclem32  40801  etransclem35  40804  sge0reval  40907  sge0sn  40914  nnfoctbdjlem  40990  isomenndlem  41065  ovnn0val  41086  ovnsubaddlem1  41105  hoidmvn0val  41119  hsphoidmvle2  41120  hsphoidmvle  41121  hoidmvval0  41122  hoidmv1lelem2  41127  hoidmvlelem2  41131  hoidmvlelem3  41132  ovnhoilem1  41136  hspmbllem1  41161  hspmbllem2  41162  volico2  41176  ovolval2lem  41178  ovnsubadd2lem  41180  ovolval4lem1  41184  ovnovollem3  41193  vonioo  41217  vonicc  41220  fdmdifeqresdif  42445  dig1  42727  dignn0flhalflem1  42734
  Copyright terms: Public domain W3C validator