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

Theorem iffalsed 4047
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 4045 . 2 𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐵)
31, 2syl 17 1 (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1475  ifcif 4036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037
This theorem is referenced by:  ifeqor  4082  ifnot  4083  ifan  4084  somincom  5449  mpt2difsnif  6651  tz7.44-2  7390  tz7.44-3  7391  unxpdomlem2  8050  sniffsupp  8198  unwdomg  8372  cantnfp1lem1  8458  cantnfp1lem3  8460  cantnflem1d  8468  ttukeylem7  9220  canthp1lem2  9354  pwfseqlem3  9361  xmulneg1  11971  rexmul  11973  xmulpnf1  11976  fzprval  12271  expnnval  12725  expneg  12730  ccatval2  13215  ccatalpha  13228  swrdnd  13284  swrdnd2  13285  swrd0  13286  swrdccatin2  13338  relexpsucnnr  13613  relexp1g  13614  sgnp  13678  sgnn  13682  absmax  13917  sumss2  14304  fsumsplit  14318  fprodntriv  14511  fprodsplit  14535  ef0lem  14648  rpnnen2lem9  14790  sadadd2  15020  eucalgf  15134  eucalginv  15135  eucalglt  15136  iserodd  15378  pcmpt  15434  pcmpt2  15435  ramtub  15554  gsumval2a  17102  mgm2nsgrplem2  17229  mgm2nsgrplem3  17230  sgrp2nmndlem3  17235  mulgnn  17370  mulgnegnn  17374  symgextfv  17661  pmtrprfv3  17697  pmtrdifellem4  17722  pmtrprfval  17730  pmtrprfvalrn  17731  odlem2  17781  dfod2  17804  gsumval3a  18127  gsumzsplit  18150  dmdprdsplitlem  18259  abvtrivd  18663  psrlidm  19224  psrridm  19225  mvrcl  19270  mplmon  19284  mplmonmul  19285  mplcoe1  19286  mplcoe5  19289  evlslem3  19335  coe1tmfv2  19466  cply1coe0  19490  cply1coe0bi  19491  gsummoncoe1  19495  uvcvv0  19948  uvcff  19949  mulmarep1gsum1  20198  1marepvsma1  20208  mdetunilem2  20238  mdetunilem9  20245  maducoeval2  20265  symgmatr01lem  20278  gsummatr01lem3  20282  gsummatr01lem4  20283  gsummatr01  20284  m2cpm  20365  m2cpminvid2lem  20378  pmatcollpw3fi1lem1  20410  mp2pm2mplem4  20433  chfacffsupp  20480  chfacfscmul0  20482  chfacfpmmul0  20486  ptpjpre2  21193  ptopn2  21197  xkopt  21268  tsmssplit  21765  xrsxmet  22420  htpycc  22587  pco1  22623  pcohtpylem  22627  pcoass  22632  pcorevlem  22634  ovolunlem1a  23071  ovolunlem1  23072  ovolicc1  23091  itg11  23264  mbfi1flim  23296  itg2split  23322  itg2cnlem1  23334  itgeq2  23350  itgss2  23385  itgss3  23387  itgless  23389  ibladdlem  23392  itgaddlem1  23395  itggt0  23414  itgcn  23415  dvexp2  23523  lhop2  23582  deg1add  23667  ig1pval3  23738  ply1termlem  23763  plyeq0lem  23770  plypf1  23772  dvply1  23843  pserdvlem2  23986  abelthlem9  23998  logtayllem  24205  logtayl  24206  cxpef  24211  rlimcnp2  24493  efrlim  24496  muinv  24719  bposlem5  24813  lgsval2lem  24832  lgsval4  24842  lgsval4a  24844  lgsneg  24846  lgsneg1  24847  lgsdilem  24849  lgsdir  24857  lgsne0  24860  gausslemma2dlem1a  24890  gausslemma2dlem3  24893  2lgslem3  24929  rplogsumlem2  24974  dchrisum0fno1  25000  rplogsum  25016  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  padicabv  25119  ostth1  25122  ostth3  25127  axlowdim  25641  funvtxdm2val  25688  funiedgdm2val  25689  funvtxdmge2val  25691  funiedgdmge2val  25692  snstrvtxval  25712  snstriedgval  25713  clwlkisclwwlklem2fv2  26311  partfun  28858  psgnfzto1stlem  29181  smattr  29193  smatbl  29194  smatbr  29195  1smat1  29198  submatminr1  29204  madjusmdetlem1  29221  madjusmdetlem2  29222  xrge0iifcv  29308  xrge0iif1  29312  ind0  29409  esumpinfval  29462  sigaclfu2  29511  eulerpartlemgs2  29769  ballotlemrv2  29910  signswmnd  29960  signswlid  29962  signsvtp  29986  signlem0  29990  mrsubcn  30670  bcneg1  30875  bccolsum  30878  dfrdg2  30945  dfrdg4  31228  unblimceq0lem  31667  unbdqndv2lem2  31671  finxpreclem3  32406  finxpreclem5  32408  poimirlem1  32580  poimirlem2  32581  poimirlem7  32586  poimirlem10  32589  poimirlem11  32590  poimirlem16  32595  poimirlem17  32596  poimirlem20  32599  poimirlem24  32603  mblfinlem2  32617  itg2addnclem2  32632  ibladdnclem  32636  ftc1anclem6  32660  ftc1anclem8  32662  fdc  32711  heiborlem6  32785  cdleme31fv2  34699  cdlemefr27cl  34709  kelac1  36651  flcidc  36763  relexp01min  37024  relexpxpmin  37028  clsk1indlem0  37359  refsum2cnlem1  38219  upbdrech2  38463  ssfiunibd  38464  ioondisj2  38561  icccncfext  38773  cncfiooicclem1  38779  cncfioobdlem  38782  dvnxpaek  38832  dvnprodlem1  38836  ditgeqiooicc  38852  iblcncfioo  38870  volioore  38883  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem40  39040  fourierdlem56  39055  fourierdlem65  39064  fourierdlem66  39065  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem78  39077  fourierdlem79  39078  fourierdlem81  39080  fourierdlem82  39081  fourierdlem97  39096  fourierdlem103  39102  fourierdlem104  39103  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  etransclem4  39131  etransclem14  39141  etransclem20  39147  etransclem22  39149  etransclem24  39151  etransclem25  39152  etransclem31  39158  etransclem32  39159  etransclem35  39162  sge0reval  39265  sge0sn  39272  nnfoctbdjlem  39348  isomenndlem  39420  ovnn0val  39441  ovnsubaddlem1  39460  hoidmvn0val  39474  hsphoidmvle2  39475  hsphoidmvle  39476  hoidmvval0  39477  hoidmv1lelem2  39482  hoidmvlelem2  39486  hoidmvlelem3  39487  ovnhoilem1  39491  hspmbllem1  39516  hspmbllem2  39517  volico2  39531  ovolval2lem  39533  ovnsubadd2lem  39535  ovolval4lem1  39539  ovnovollem3  39548  vonioo  39573  vonicc  39576  crctcsh1wlkn0lem3  41015  crctcsh  41027  clwlkclwwlklem2fv2  41205  eucrct2eupth  41413  fdmdifeqresdif  41913  dig1  42200  dignn0flhalflem1  42207
  Copyright terms: Public domain W3C validator