Theorem iftrued 3949

Description: Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

Ref	Expression
iftrued.1

Assertion

Ref	Expression
iftrued

Proof of Theorem iftrued

Step	Hyp	Ref	Expression
1		iftrued.1	. 2
2		iftrue 3947	. 2
3	1, 2	syl 16	1

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

This theorem is referenced by:  mpt2snif  6396  tz7.44-3  7093  iunfictbso  8516  ttukeylem7  8916  max0sub  11424  ifle  11425  xmulneg1  11490  xmulpnf1  11495  expnnval  12169  lswccat0lsw  12608  swrdval2  12647  swrdlend  12656  swrd0  12658  swrdccatid  12722  max0add  13143  summolem2a  13537  prodmolem2a  13741  ef0lem  13814  rpnnen2lem3  13950  rpnnen2lem9  13956  iserodd  14359  pcmpt  14411  pcmpt2  14412  setcepi  15415  gsumval2a  15906  mgm2nsgrplem3  16038  mulgnn  16148  pmtrprfv  16478  pmtrprfval  16512  psgnunilem1  16518  dfod2  16586  oddvds2  16588  cyggenod  16887  mplcoe1  18127  mplcoe5  18131  coe1tm  18314  coe1tmmul2fv  18319  coe1pwmulfv  18321  coe1sclmul  18323  coe1sclmul2  18325  m1detdiag  19099  mdetunilem9  19122  maducoeval2  19142  symgmatr01lem  19155  pmatcollpw3fi1lem1  19287  chpmat1dlem  19336  chfacffsupp  19357  chfacfscmul0  19359  chfacfpmmul0  19363  2ndcdisj  19957  dscmet  21093  xrsxmet  21314  cnmpt2pc  21428  xrhmeo  21446  oprpiece1res1  21451  htpycc  21480  pcoval1  21513  pcohtpylem  21519  pcoass  21524  pcorevlem  21526  ovolunlem1a  21907  ovolunlem1  21908  ovolicc2lem3  21930  ovolicc2lem4  21931  mbfi1fseqlem4  22125  mbfi1fseqlem5  22126  mbfi1fseqlem6  22127  itg2const2  22148  itg2splitlem  22155  itg2split  22156  itg2cnlem1  22168  itg2cnlem2  22169  iblss2  22212  itgspliticc  22243  ditgpos  22260  limcres  22290  plyeq0lem  22607  plypf1  22609  coeeq2  22639  dvply1  22680  aareccl  22722  dvtaylp  22765  pserdvlem2  22823  isppw  23388  vmappw  23390  muval1  23407  dchrelbasd  23514  dchr1  23532  dchrptlem2  23540  lgsdir2  23603  lgsne0  23608  rplogsumlem2  23670  dchrisum0flblem2  23694  dchrisum0fno1  23696  rplogsum  23712  pntrlog2bndlem5  23766  clwlkisclwwlklem2fv1  24782  eupath2  24980  gxpval  25261  partfun  27516  ofldchr  27804  esumpinfval  28079  eulerpartlemgs2  28319  ballotlemsgt1  28449  ballotlemsel1i  28451  ballotlemsi  28453  signswmnd  28514  signsvtn  28541  lgamgulmlem4  28574  cvmliftlem10  28739  itg2addnc  30069  itg2gt0cn  30070  itgaddnclem2  30074  sdclem1  30236  flcidc  31123  ioondisj2  31525  ioondisj1  31526  lptioo1  31638  icccncfext  31690  cncfiooicc  31697  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnxpaek  31739  ditgeq3d  31763  itgsubsticclem  31774  dirkerper  31878  dirkercncflem2  31886  fourierdlem40  31929  fourierdlem65  31954  fourierdlem74  31963  fourierdlem75  31964  fourierdlem78  31967  fourierdlem81  31970  fourierdlem97  31986  fourierdlem103  31992  fourierdlem104  31993  sqwvfoura  32011  sqwvfourb  32012  fourierswlem  32013  fouriersw  32014  elaa2lem  32016  etransclem19  32036  etransclem22  32039  etransclem24  32041  etransclem35  32052  cdlemefs27cl  36139

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