Theorem iffalsed 3952

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

Proof of Theorem iffalsed

Step	Hyp	Ref	Expression
1		iffalsed.1	. 2
2		iffalse 3950	. 2
3	1, 2	syl 16	1

Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  ifcif 3941

This theorem is referenced by:  ifeqor  3985  ifnot  3986  ifan  3987  somincom  5409  mpt2difsnif  6395  tz7.44-2  7092  tz7.44-3  7093  unxpdomlem2  7745  sniffsupp  7889  unwdomg  8031  cantnfp1lem1  8118  cantnfp1lem3  8120  cantnflem1d  8128  ttukeylem7  8916  canthp1lem2  9052  pwfseqlem3  9059  xmulneg1  11490  rexmul  11492  xmulpnf1  11495  fzprval  11769  expnnval  12169  expneg  12174  ccatval2  12596  lswccatn0lsw  12607  swrdnd  12657  swrd0  12658  swrdvalodm2  12664  swrdvalodm  12665  swrdccatin2  12712  sgnp  12923  sgnn  12927  absmax  13162  sumss2  13548  fsumsplit  13562  fprodntriv  13749  fprodsplit  13770  ef0lem  13814  rpnnen2lem9  13956  sadadd2  14110  eucalgf  14212  eucalginv  14213  eucalglt  14214  iserodd  14359  pcmpt  14411  pcmpt2  14412  ramtub  14530  gsumval2a  15906  mgm2nsgrplem2  16037  mgm2nsgrplem3  16038  sgrp2nmndlem3  16043  mulgnn  16148  mulgnegnn  16152  symgextfv  16443  pmtrprfv3  16479  pmtrdifellem4  16504  pmtrprfval  16512  pmtrprfvalrn  16513  odlem2  16563  dfod2  16586  gsumval3a  16905  gsumzsplit  16944  dmdprdsplitlem  17084  abvtrivd  17489  psrlidm  18056  psrridm  18058  mvrcl  18111  mplmon  18125  mplmonmul  18126  mplcoe1  18127  mplcoe5  18131  evlslem3  18183  coe1tmfv2  18316  cply1coe0  18341  cply1coe0bi  18342  gsummoncoe1  18346  uvcvv0  18821  uvcff  18822  mulmarep1gsum1  19075  1marepvsma1  19085  mdetunilem2  19115  mdetunilem9  19122  maducoeval2  19142  symgmatr01lem  19155  gsummatr01lem3  19159  gsummatr01lem4  19160  gsummatr01  19161  m2cpm  19242  m2cpminvid2lem  19255  pmatcollpw3fi1lem1  19287  mp2pm2mplem4  19310  chfacffsupp  19357  chfacfscmul0  19359  chfacfpmmul0  19363  ptpjpre2  20081  ptopn2  20085  xkopt  20156  tsmssplit  20654  xrsxmet  21314  htpycc  21480  pco1  21515  pcohtpylem  21519  pcoass  21524  pcorevlem  21526  ovolunlem1a  21907  ovolunlem1  21908  ovolicc1  21927  itg11  22098  mbfi1flim  22130  itg2split  22156  itg2cnlem1  22168  itgeq2  22184  itgss2  22219  itgss3  22221  itgless  22223  ibladdlem  22226  itgaddlem1  22229  itggt0  22248  itgcn  22249  dvexp2  22357  lhop2  22416  deg1add  22504  ig1pval3  22575  ply1termlem  22600  plyeq0lem  22607  plypf1  22609  dvply1  22680  pserdvlem2  22823  abelthlem9  22835  logtayllem  23040  logtayl  23041  cxpef  23046  rlimcnp2  23296  efrlim  23299  muinv  23469  bposlem5  23563  lgsval2lem  23581  lgsval4  23591  lgsval4a  23593  lgsneg  23594  lgsneg1  23595  lgsdilem  23597  lgsdir  23605  lgsne0  23608  rplogsumlem2  23670  dchrisum0fno1  23696  rplogsum  23712  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  padicabv  23815  ostth1  23818  ostth3  23823  axlowdim  24264  clwlkisclwwlklem2fv2  24783  gxpval  25261  gxnval  25262  partfun  27516  xrge0iifcv  27916  xrge0iif1  27920  ind0  28033  esumpinfval  28079  sigaclfu2  28121  eulerpartlemgs2  28319  ballotlemrv2  28460  signswmnd  28514  signswlid  28516  signsvtp  28540  signlem0  28544  mrsubcn  28879  dfrdg2  29228  dfrdg4  29600  mblfinlem2  30052  itg2addnclem2  30067  ibladdnclem  30071  ftc1anclem6  30095  ftc1anclem8  30097  fdc  30238  heiborlem6  30312  kelac1  31009  flcidc  31123  refsum2cnlem1  31412  upbdrech2  31508  ssfiunibd  31509  ioondisj2  31525  icccncfext  31690  cncfiooicclem1  31696  cncfioobdlem  31699  dvnxpaek  31739  dvnprodlem1  31743  ditgeqiooicc  31759  iblcncfioo  31777  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem40  31929  fourierdlem56  31945  fourierdlem65  31954  fourierdlem66  31955  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem78  31967  fourierdlem79  31968  fourierdlem81  31970  fourierdlem82  31971  fourierdlem97  31986  fourierdlem103  31992  fourierdlem104  31993  sqwvfoura  32011  sqwvfourb  32012  fourierswlem  32013  fouriersw  32014  etransclem4  32021  etransclem14  32031  etransclem20  32037  etransclem22  32039  etransclem24  32041  etransclem25  32042  etransclem31  32048  etransclem32  32049  etransclem35  32052  fdmdifeqresdif  32931  cdleme31fv2  36119  cdlemefr27cl  36129

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-if 3942