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

Theorem iffalsed 3895
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 3893 . 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 1405   ifcif 3884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-if 3885
This theorem is referenced by:  ifeqor  3928  ifnot  3929  ifan  3930  somincom  5221  mpt2difsnif  6375  tz7.44-2  7109  tz7.44-3  7110  unxpdomlem2  7759  sniffsupp  7902  unwdomg  8043  cantnfp1lem1  8128  cantnfp1lem3  8130  cantnflem1d  8138  ttukeylem7  8926  canthp1lem2  9060  pwfseqlem3  9067  xmulneg1  11513  rexmul  11515  xmulpnf1  11518  fzprval  11793  expnnval  12211  expneg  12216  ccatval2  12648  swrdnd  12711  swrdnd2  12712  swrd0  12713  swrdccatin2  12766  relexpsucnnr  13005  relexp1g  13006  sgnp  13070  sgnn  13074  absmax  13309  sumss2  13695  fsumsplit  13709  fprodntriv  13899  fprodsplit  13920  ef0lem  14021  rpnnen2lem9  14163  sadadd2  14317  eucalgf  14419  eucalginv  14420  eucalglt  14421  iserodd  14566  pcmpt  14618  pcmpt2  14619  ramtub  14737  gsumval2a  16228  mgm2nsgrplem2  16359  mgm2nsgrplem3  16360  sgrp2nmndlem3  16365  mulgnn  16470  mulgnegnn  16474  symgextfv  16765  pmtrprfv3  16801  pmtrdifellem4  16826  pmtrprfval  16834  pmtrprfvalrn  16835  odlem2  16885  dfod2  16908  gsumval3a  17227  gsumzsplit  17266  dmdprdsplitlem  17402  abvtrivd  17807  psrlidm  18374  psrridm  18376  mvrcl  18429  mplmon  18443  mplmonmul  18444  mplcoe1  18445  mplcoe5  18449  evlslem3  18501  coe1tmfv2  18634  cply1coe0  18659  cply1coe0bi  18660  gsummoncoe1  18664  uvcvv0  19115  uvcff  19116  mulmarep1gsum1  19365  1marepvsma1  19375  mdetunilem2  19405  mdetunilem9  19412  maducoeval2  19432  symgmatr01lem  19445  gsummatr01lem3  19449  gsummatr01lem4  19450  gsummatr01  19451  m2cpm  19532  m2cpminvid2lem  19545  pmatcollpw3fi1lem1  19577  mp2pm2mplem4  19600  chfacffsupp  19647  chfacfscmul0  19649  chfacfpmmul0  19653  ptpjpre2  20371  ptopn2  20375  xkopt  20446  tsmssplit  20944  xrsxmet  21604  htpycc  21770  pco1  21805  pcohtpylem  21809  pcoass  21814  pcorevlem  21816  ovolunlem1a  22197  ovolunlem1  22198  ovolicc1  22217  itg11  22388  mbfi1flim  22420  itg2split  22446  itg2cnlem1  22458  itgeq2  22474  itgss2  22509  itgss3  22511  itgless  22513  ibladdlem  22516  itgaddlem1  22519  itggt0  22538  itgcn  22539  dvexp2  22647  lhop2  22706  deg1add  22794  ig1pval3  22865  ply1termlem  22890  plyeq0lem  22897  plypf1  22899  dvply1  22970  pserdvlem2  23113  abelthlem9  23125  logtayllem  23332  logtayl  23333  cxpef  23338  rlimcnp2  23620  efrlim  23623  muinv  23848  bposlem5  23942  lgsval2lem  23960  lgsval4  23970  lgsval4a  23972  lgsneg  23973  lgsneg1  23974  lgsdilem  23976  lgsdir  23984  lgsne0  23987  rplogsumlem2  24049  dchrisum0fno1  24075  rplogsum  24091  pntrlog2bndlem4  24144  pntrlog2bndlem5  24145  padicabv  24194  ostth1  24197  ostth3  24202  axlowdim  24668  clwlkisclwwlklem2fv2  25187  gxpval  25661  gxnval  25662  partfun  27946  xrge0iifcv  28355  xrge0iif1  28359  ind0  28453  esumpinfval  28506  sigaclfu2  28555  eulerpartlemgs2  28811  ballotlemrv2  28952  signswmnd  29006  signswlid  29008  signsvtp  29032  signlem0  29036  mrsubcn  29718  bcneg1  29932  bccolsum  29935  dfrdg2  30002  dfrdg4  30276  mblfinlem2  31404  itg2addnclem2  31420  ibladdnclem  31424  ftc1anclem6  31448  ftc1anclem8  31450  fdc  31500  heiborlem6  31574  cdleme31fv2  33392  cdlemefr27cl  33402  kelac1  35351  flcidc  35467  relexp01min  35672  relexpxpmin  35676  refsum2cnlem1  36772  upbdrech2  36857  ssfiunibd  36858  ioondisj2  36874  icccncfext  37039  cncfiooicclem1  37045  cncfioobdlem  37048  dvnxpaek  37088  dvnprodlem1  37092  ditgeqiooicc  37108  iblcncfioo  37126  dirkercncflem2  37235  dirkercncflem4  37237  fourierdlem40  37278  fourierdlem56  37294  fourierdlem65  37303  fourierdlem66  37304  fourierdlem73  37311  fourierdlem74  37312  fourierdlem75  37313  fourierdlem78  37316  fourierdlem79  37317  fourierdlem81  37319  fourierdlem82  37320  fourierdlem97  37335  fourierdlem103  37341  fourierdlem104  37342  sqwvfoura  37360  sqwvfourb  37361  fourierswlem  37362  fouriersw  37363  etransclem4  37370  etransclem14  37380  etransclem20  37386  etransclem22  37388  etransclem24  37390  etransclem25  37391  etransclem31  37397  etransclem32  37398  etransclem35  37401  fdmdifeqresdif  38423  dig1  38720  dignn0flhalflem1  38727
  Copyright terms: Public domain W3C validator