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

Theorem iffalsed 3922
Description: Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
iffalsed.1  |-  ( ph  ->  -.  ch )
Assertion
Ref Expression
iffalsed  |-  ( ph  ->  if ( ch ,  A ,  B )  =  B )

Proof of Theorem iffalsed
StepHypRef Expression
1 iffalsed.1 . 2  |-  ( ph  ->  -.  ch )
2 iffalse 3920 . 2  |-  ( -. 
ch  ->  if ( ch ,  A ,  B
)  =  B )
31, 2syl 17 1  |-  ( ph  ->  if ( ch ,  A ,  B )  =  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1437   ifcif 3911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-if 3912
This theorem is referenced by:  ifeqor  3955  ifnot  3956  ifan  3957  somincom  5253  mpt2difsnif  6403  tz7.44-2  7136  tz7.44-3  7137  unxpdomlem2  7786  sniffsupp  7932  unwdomg  8108  cantnfp1lem1  8191  cantnfp1lem3  8193  cantnflem1d  8201  ttukeylem7  8952  canthp1lem2  9085  pwfseqlem3  9092  xmulneg1  11562  rexmul  11564  xmulpnf1  11567  fzprval  11863  expnnval  12281  expneg  12286  ccatval2  12727  swrdnd  12790  swrdnd2  12791  swrd0  12792  swrdccatin2  12845  relexpsucnnr  13088  relexp1g  13089  sgnp  13153  sgnn  13157  absmax  13392  sumss2  13791  fsumsplit  13805  fprodntriv  13995  fprodsplit  14019  ef0lem  14132  rpnnen2lem9  14274  sadadd2  14433  eucalgf  14541  eucalginv  14542  eucalglt  14543  iserodd  14784  pcmpt  14836  pcmpt2  14837  ramtub  14967  ramtubOLD  14968  gsumval2a  16521  mgm2nsgrplem2  16652  mgm2nsgrplem3  16653  sgrp2nmndlem3  16658  mulgnn  16763  mulgnegnn  16767  symgextfv  17058  pmtrprfv3  17094  pmtrdifellem4  17119  pmtrprfval  17127  pmtrprfvalrn  17128  odlem2  17187  odlem2OLD  17203  dfod2  17214  gsumval3a  17536  gsumzsplit  17559  dmdprdsplitlem  17669  abvtrivd  18067  psrlidm  18626  psrridm  18627  mvrcl  18672  mplmon  18686  mplmonmul  18687  mplcoe1  18688  mplcoe5  18691  evlslem3  18736  coe1tmfv2  18867  cply1coe0  18892  cply1coe0bi  18893  gsummoncoe1  18897  uvcvv0  19346  uvcff  19347  mulmarep1gsum1  19596  1marepvsma1  19606  mdetunilem2  19636  mdetunilem9  19643  maducoeval2  19663  symgmatr01lem  19676  gsummatr01lem3  19680  gsummatr01lem4  19681  gsummatr01  19682  m2cpm  19763  m2cpminvid2lem  19776  pmatcollpw3fi1lem1  19808  mp2pm2mplem4  19831  chfacffsupp  19878  chfacfscmul0  19880  chfacfpmmul0  19884  ptpjpre2  20593  ptopn2  20597  xkopt  20668  tsmssplit  21164  xrsxmet  21825  htpycc  22009  pco1  22044  pcohtpylem  22048  pcoass  22053  pcorevlem  22055  ovolunlem1a  22447  ovolunlem1  22448  ovolicc1  22467  itg11  22647  mbfi1flim  22679  itg2split  22705  itg2cnlem1  22717  itgeq2  22733  itgss2  22768  itgss3  22770  itgless  22772  ibladdlem  22775  itgaddlem1  22778  itggt0  22797  itgcn  22798  dvexp2  22906  lhop2  22965  deg1add  23050  ig1pval3  23124  ig1pval3OLD  23130  ply1termlem  23155  plyeq0lem  23162  plypf1  23164  dvply1  23235  pserdvlem2  23381  abelthlem9  23393  logtayllem  23602  logtayl  23603  cxpef  23608  rlimcnp2  23890  efrlim  23893  muinv  24120  bposlem5  24214  lgsval2lem  24232  lgsval4  24242  lgsval4a  24244  lgsneg  24245  lgsneg1  24246  lgsdilem  24248  lgsdir  24256  lgsne0  24259  rplogsumlem2  24321  dchrisum0fno1  24347  rplogsum  24363  pntrlog2bndlem4  24416  pntrlog2bndlem5  24417  padicabv  24466  ostth1  24469  ostth3  24474  axlowdim  24989  clwlkisclwwlklem2fv2  25509  gxpval  25985  gxnval  25986  partfun  28280  psgnfzto1stlem  28621  smattr  28633  smatbl  28634  smatbr  28635  1smat1  28638  submatminr1  28644  madjusmdetlem1  28661  madjusmdetlem2  28662  xrge0iifcv  28748  xrge0iif1  28752  ind0  28849  esumpinfval  28902  sigaclfu2  28951  eulerpartlemgs2  29221  ballotlemrv2  29362  ballotlemrv2OLD  29400  signswmnd  29454  signswlid  29456  signsvtp  29480  signlem0  29484  mrsubcn  30165  bcneg1  30379  bccolsum  30382  dfrdg2  30449  dfrdg4  30723  finxpreclem3  31749  finxpreclem5  31751  poimirlem1  31905  poimirlem2  31906  poimirlem7  31911  poimirlem10  31914  poimirlem11  31915  poimirlem16  31920  poimirlem17  31921  poimirlem20  31924  poimirlem24  31928  mblfinlem2  31942  itg2addnclem2  31958  ibladdnclem  31962  ftc1anclem6  31986  ftc1anclem8  31988  fdc  32038  heiborlem6  32112  cdleme31fv2  33929  cdlemefr27cl  33939  kelac1  35891  flcidc  36010  relexp01min  36275  relexpxpmin  36279  refsum2cnlem1  37331  upbdrech2  37480  ssfiunibd  37481  ioondisj2  37538  icccncfext  37705  cncfiooicclem1  37711  cncfioobdlem  37714  dvnxpaek  37757  dvnprodlem1  37761  ditgeqiooicc  37777  iblcncfioo  37795  dirkercncflem2  37906  dirkercncflem4  37908  fourierdlem40  37950  fourierdlem56  37966  fourierdlem65  37975  fourierdlem66  37976  fourierdlem73  37983  fourierdlem74  37984  fourierdlem75  37985  fourierdlem78  37988  fourierdlem79  37989  fourierdlem81  37991  fourierdlem82  37992  fourierdlem97  38007  fourierdlem103  38013  fourierdlem104  38014  sqwvfoura  38032  sqwvfourb  38033  fourierswlem  38034  fouriersw  38035  etransclem4  38043  etransclem14  38053  etransclem20  38059  etransclem22  38061  etransclem24  38063  etransclem25  38064  etransclem31  38070  etransclem32  38071  etransclem35  38074  sge0reval  38122  sge0sn  38129  nnfoctbdjlem  38201  isomenndlem  38259  ovnn0val  38277  ovnsubaddlem1  38296  hoidmvn0val  38310  hsphoidmvle2  38311  hsphoidmvle  38312  hoidmvval0  38313  hoidmv1lelem2  38318  hoidmvlelem2  38322  hoidmvlelem3  38323  ovnhoilem1  38327  funvtxdm2val  38943  funiedgdm2val  38944  funvtxdmge2val  38945  funiedgdmge2val  38946  funiedgval  38951  snstrvtxval  38966  snstriedgval  38967  fdmdifeqresdif  39744  dig1  40040  dignn0flhalflem1  40047
  Copyright terms: Public domain W3C validator