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

Theorem iffalsed 3904
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 3902 . 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 1455   ifcif 3893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-if 3894
This theorem is referenced by:  ifeqor  3937  ifnot  3938  ifan  3939  somincom  5256  mpt2difsnif  6421  tz7.44-2  7156  tz7.44-3  7157  unxpdomlem2  7808  sniffsupp  7954  unwdomg  8130  cantnfp1lem1  8214  cantnfp1lem3  8216  cantnflem1d  8224  ttukeylem7  8976  canthp1lem2  9109  pwfseqlem3  9116  xmulneg1  11589  rexmul  11591  xmulpnf1  11594  fzprval  11891  expnnval  12313  expneg  12318  ccatval2  12765  swrdnd  12831  swrdnd2  12832  swrd0  12833  swrdccatin2  12886  relexpsucnnr  13143  relexp1g  13144  sgnp  13208  sgnn  13212  absmax  13447  sumss2  13847  fsumsplit  13861  fprodntriv  14051  fprodsplit  14075  ef0lem  14188  rpnnen2lem9  14330  sadadd2  14489  eucalgf  14597  eucalginv  14598  eucalglt  14599  iserodd  14840  pcmpt  14892  pcmpt2  14893  ramtub  15023  ramtubOLD  15024  gsumval2a  16577  mgm2nsgrplem2  16708  mgm2nsgrplem3  16709  sgrp2nmndlem3  16714  mulgnn  16819  mulgnegnn  16823  symgextfv  17114  pmtrprfv3  17150  pmtrdifellem4  17175  pmtrprfval  17183  pmtrprfvalrn  17184  odlem2  17243  odlem2OLD  17259  dfod2  17270  gsumval3a  17592  gsumzsplit  17615  dmdprdsplitlem  17725  abvtrivd  18123  psrlidm  18682  psrridm  18683  mvrcl  18728  mplmon  18742  mplmonmul  18743  mplcoe1  18744  mplcoe5  18747  evlslem3  18792  coe1tmfv2  18923  cply1coe0  18948  cply1coe0bi  18949  gsummoncoe1  18953  uvcvv0  19403  uvcff  19404  mulmarep1gsum1  19653  1marepvsma1  19663  mdetunilem2  19693  mdetunilem9  19700  maducoeval2  19720  symgmatr01lem  19733  gsummatr01lem3  19737  gsummatr01lem4  19738  gsummatr01  19739  m2cpm  19820  m2cpminvid2lem  19833  pmatcollpw3fi1lem1  19865  mp2pm2mplem4  19888  chfacffsupp  19935  chfacfscmul0  19937  chfacfpmmul0  19941  ptpjpre2  20650  ptopn2  20654  xkopt  20725  tsmssplit  21221  xrsxmet  21882  htpycc  22066  pco1  22101  pcohtpylem  22105  pcoass  22110  pcorevlem  22112  ovolunlem1a  22504  ovolunlem1  22505  ovolicc1  22524  itg11  22705  mbfi1flim  22737  itg2split  22763  itg2cnlem1  22775  itgeq2  22791  itgss2  22826  itgss3  22828  itgless  22830  ibladdlem  22833  itgaddlem1  22836  itggt0  22855  itgcn  22856  dvexp2  22964  lhop2  23023  deg1add  23108  ig1pval3  23182  ig1pval3OLD  23188  ply1termlem  23213  plyeq0lem  23220  plypf1  23222  dvply1  23293  pserdvlem2  23439  abelthlem9  23451  logtayllem  23660  logtayl  23661  cxpef  23666  rlimcnp2  23948  efrlim  23951  muinv  24178  bposlem5  24272  lgsval2lem  24290  lgsval4  24300  lgsval4a  24302  lgsneg  24303  lgsneg1  24304  lgsdilem  24306  lgsdir  24314  lgsne0  24317  rplogsumlem2  24379  dchrisum0fno1  24405  rplogsum  24421  pntrlog2bndlem4  24474  pntrlog2bndlem5  24475  padicabv  24524  ostth1  24527  ostth3  24532  axlowdim  25047  clwlkisclwwlklem2fv2  25567  gxpval  26043  gxnval  26044  partfun  28330  psgnfzto1stlem  28664  smattr  28676  smatbl  28677  smatbr  28678  1smat1  28681  submatminr1  28687  madjusmdetlem1  28704  madjusmdetlem2  28705  xrge0iifcv  28791  xrge0iif1  28795  ind0  28892  esumpinfval  28945  sigaclfu2  28994  eulerpartlemgs2  29263  ballotlemrv2  29404  ballotlemrv2OLD  29442  signswmnd  29496  signswlid  29498  signsvtp  29522  signlem0  29526  mrsubcn  30207  bcneg1  30422  bccolsum  30425  dfrdg2  30492  dfrdg4  30768  finxpreclem3  31831  finxpreclem5  31833  poimirlem1  31987  poimirlem2  31988  poimirlem7  31993  poimirlem10  31996  poimirlem11  31997  poimirlem16  32002  poimirlem17  32003  poimirlem20  32006  poimirlem24  32010  mblfinlem2  32024  itg2addnclem2  32040  ibladdnclem  32044  ftc1anclem6  32068  ftc1anclem8  32070  fdc  32120  heiborlem6  32194  cdleme31fv2  34006  cdlemefr27cl  34016  kelac1  35967  flcidc  36086  relexp01min  36351  relexpxpmin  36355  refsum2cnlem1  37399  upbdrech2  37601  ssfiunibd  37602  ioondisj2  37674  icccncfext  37851  cncfiooicclem1  37857  cncfioobdlem  37860  dvnxpaek  37903  dvnprodlem1  37907  ditgeqiooicc  37923  iblcncfioo  37941  volioore  37954  dirkercncflem2  38067  dirkercncflem4  38069  fourierdlem40  38111  fourierdlem56  38127  fourierdlem65  38136  fourierdlem66  38137  fourierdlem73  38144  fourierdlem74  38145  fourierdlem75  38146  fourierdlem78  38149  fourierdlem79  38150  fourierdlem81  38152  fourierdlem82  38153  fourierdlem97  38168  fourierdlem103  38174  fourierdlem104  38175  sqwvfoura  38193  sqwvfourb  38194  fourierswlem  38195  fouriersw  38196  etransclem4  38204  etransclem14  38214  etransclem20  38220  etransclem22  38222  etransclem24  38224  etransclem25  38225  etransclem31  38231  etransclem32  38232  etransclem35  38235  sge0reval  38317  sge0sn  38324  nnfoctbdjlem  38398  isomenndlem  38459  ovnn0val  38480  ovnsubaddlem1  38499  hoidmvn0val  38513  hsphoidmvle2  38514  hsphoidmvle  38515  hoidmvval0  38516  hoidmv1lelem2  38521  hoidmvlelem2  38525  hoidmvlelem3  38526  ovnhoilem1  38530  hspmbllem1  38555  hspmbllem2  38556  volico2  38570  ovolval2lem  38572  ovnsubadd2lem  38574  ovolval4lem1  38578  ovnovollem3  38587  funvtxdm2val  39255  funiedgdm2val  39256  funvtxdmge2val  39258  funiedgdmge2val  39259  funiedgval  39263  snstrvtxval  39279  snstriedgval  39280  fdmdifeqresdif  40492  dig1  40788  dignn0flhalflem1  40795
  Copyright terms: Public domain W3C validator