Theorem iftrue 3947

Description: Value of the conditional operator when its first argument is true. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
iftrue

Proof of Theorem iftrue

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dedlem0a 952	. . 3
2	1	abbi2dv 2594	. 2
3		dfif2 3943	. 2
4	2, 3	syl6reqr 2517	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  {cab 2442  ifcif 3941

This theorem is referenced by:  iftruei  3948  iftrued  3949  ifsb  3954  ifbi  3962  ifeq2da  3972  ifclda  3973  ifeqda  3974  elimif  3975  ifbothda  3976  ifid  3978  ifeqor  3985  ifnot  3986  ifan  3987  ifor  3988  2if2  3989  dedth  3993  elimhyp  4000  elimhyp2v  4001  elimhyp3v  4002  elimhyp4v  4003  elimdhyp  4005  keephyp2v  4007  keephyp3v  4008  dfopif  4214  dfopg  4215  somin1  5408  somincom  5409  xpima1  5455  dfiota4  5584  elimdelov  6378  ovif12  6381  tz7.44-1  7091  resixpfo  7527  boxriin  7531  boxcutc  7532  pw2f1olem  7641  unxpdomlem2  7745  unxpdomlem3  7746  ordtypelem1  7964  wemaplem2  7993  unwdomg  8031  ixpiunwdom  8038  cantnfp1lem2  8119  cantnfp1lem3  8120  cantnfp1lem2OLD  8145  cantnfp1lem3OLD  8146  acndom  8453  dfac12lem2  8545  fin23lem14  8734  axcc2lem  8837  pwfseqlem2  9058  uzin  11142  xrmax1  11405  xrmax2  11406  xrmin1  11407  xrmin2  11408  max1ALT  11416  max0sub  11424  ifle  11425  xmulneg1  11490  fzprval  11769  fztpval  11770  modifeq2int  12049  seqf1olem1  12146  seqf1olem2  12147  bcval2  12383  ccatval1  12595  swrdccat  12718  swrdccat3a  12719  swrdccat3b  12721  repswswrd  12756  cshword  12762  0csh0  12764  ccatco  12801  sgnn  12927  max0add  13143  absmax  13162  sumrblem  13533  fsumcvg  13534  summolem2a  13537  isum  13541  sumss  13546  sumss2  13548  fsumcvg2  13549  fsumser  13552  fsumsplit  13562  sumsplit  13583  prodrblem  13736  fprodcvg  13737  prodmolem2a  13741  zprod  13744  iprod  13745  iprodn0  13747  prodss  13754  fprodsplit  13770  ruclem2  13965  ruclem3  13966  sadadd2lem2  14100  sadcf  14103  sadc0  14104  sadcp1  14105  sadcaddlem  14107  smupf  14128  smup0  14129  gcd0val  14147  eucalgf  14212  eucalginv  14213  eucalglt  14214  pc0  14378  pcgcd  14401  pcmptcl  14410  pcmpt  14411  pcmpt2  14412  pcprod  14414  fldivp1  14416  prmreclem2  14435  prmreclem4  14437  1arithlem4  14444  vdwlem6  14504  ramtcl2  14529  ramcl2  14534  ramub1lem1  14544  ressid2  14685  xpscfv  14959  xpsfrnel  14960  xpsaddlem  14972  xpsvsca  14976  gsumval1  15904  mgm2nsgrplem2  16037  sgrp2nmndlem2  16042  symgextfve  16444  symgfixfolem1  16463  pmtrmvd  16481  pmtrfinv  16486  pmtrprfval  16512  pmtrprfvalrn  16513  frgpuptinv  16789  frgpup2  16794  frgpup3lem  16795  cyggex  16900  gsumzsplit  16944  gsumzsplitOLD  16945  gsummpt1n0  16992  dprdfid  17057  dprdfidOLD  17064  dmdprdsplitlem  17084  dmdprdsplitlemOLD  17085  abvtrivd  17489  psrlidm  18056  psrlidmOLD  18057  psrridm  18058  psrridmOLD  18059  mvrf1  18081  mplmonmul  18126  mplcoe1  18127  mplcoe3  18128  mplcoe3OLD  18129  mplcoe5  18131  mplcoe2OLD  18133  mplmon2  18158  subrgasclcl  18164  evlslem3  18183  evlslem1  18184  coe1tmfv1  18315  ply1sclid  18329  znf1o  18590  uvcvv1  18820  dmatmul  18999  scmatscmiddistr  19010  1mavmul  19050  mulmarep1gsum2  19076  1marepvmarrepid  19077  mdetdiag  19101  mdetralt2  19111  mdetunilem2  19115  mdetunilem7  19120  mdetunilem8  19121  mdetunilem9  19122  mndifsplit  19138  maducoeval2  19142  madugsum  19145  madurid  19146  gsummatr01lem3  19159  gsummatr01  19161  smadiadetglem2  19174  1elcpmat  19216  decpmatid  19271  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  ptpjpre1  20072  ptbasfi  20082  ptpjopn  20113  isfcls  20510  ptcmplem2  20553  ptcmplem3  20554  tsmssplit  20654  dscmet  21093  dscopn  21094  icccmplem2  21328  iccpnfcnv  21444  xrhmeo  21446  pcohtpylem  21519  pcopt  21522  pcopt2  21523  pcoass  21524  pcorevlem  21526  cmetcaulem  21727  ovolicc1  21927  ioorcl  21986  i1f1lem  22096  itg11  22098  itg1addlem2  22104  itg1addlem4  22106  i1fres  22112  itg1climres  22121  mbfi1fseqlem4  22125  mbfi1fseqlem5  22126  mbfi1flim  22130  itg2const2  22148  itg2seq  22149  itg2uba  22150  itg2splitlem  22155  itg2split  22156  itg2monolem1  22157  itg2cnlem1  22168  itg2cnlem2  22169  iblcnlem  22195  iblss  22211  iblss2  22212  itgitg2  22213  itgle  22216  itgss  22218  itgss2  22219  itgss3  22221  itgless  22223  ibladdlem  22226  itgaddlem1  22229  iblabslem  22234  iblabs  22235  iblabsr  22236  iblmulc2  22237  bddmulibl  22245  itggt0  22248  itgcn  22249  limcvallem  22275  ellimc2  22281  limccnp  22295  limccnp2  22296  limcco  22297  dvcobr  22349  dvexp2  22357  elply2  22593  elplyd  22599  ply1termlem  22600  coe1termlem  22655  abelthlem9  22835  logtayl  23041  leibpilem2  23272  leibpi  23273  rlimcnp2  23296  efrlim  23299  isnsqf  23409  mule1  23422  sqff1o  23456  muinv  23469  chtublem  23486  dchrelbasd  23514  bposlem1  23559  bposlem3  23561  bposlem5  23563  bposlem6  23564  lgsval2lem  23581  lgsneg  23594  lgsdilem  23597  lgsdir2  23603  lgsdir  23605  lgsdi  23607  lgsne0  23608  dchrvmasum2if  23682  dchrvmasumiflem1  23686  rpvmasum2  23697  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  padicabv  23815  ostth2lem4  23821  axlowdimlem15  24259  ifbieq12d2  27420  elimifd  27421  elim2if  27422  resvid2  27818  xrge0iifcnv  27915  xrge0iifiso  27917  xrge0iifhom  27919  indval2  28028  ind1  28032  sigaclfu2  28121  ddeval1  28206  eulerpartlemb  28307  ballotlemsima  28454  ballotlemrv1  28459  signsw0glem  28510  signswmnd  28514  signswrid  28515  igamz  28590  indispcon  28679  mrsubvr  28871  dfrdg2  29228  dfrdg3  29229  unisnif  29575  dfrdg4  29600  mblfinlem2  30052  mbfposadd  30062  itg2addnclem  30066  itg2gt0cn  30070  ibladdnclem  30071  itgaddnclem1  30073  iblabsnclem  30078  iblabsnc  30079  iblmulc2nc  30080  bddiblnc  30085  itggt0cn  30087  ftc1anclem4  30093  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  areacirclem5  30111  areacirc  30112  fnejoin2  30187  fdc  30238  heiborlem4  30310  ac6s6  30580  pw2f1ocnv  30979  aomclem5  31004  kelac1  31009  sdrgacs  31150  phisum  31159  mon1pid  31165  arearect  31183  areaquad  31184  refsum2cnlem1  31412  upbdrech2  31508  lptioo2  31637  lptioo1  31638  coskpi2  31666  cosknegpi  31669  cncfiooicclem1  31696  cncfiooiccre  31698  dvnxpaek  31739  dvnprodlem1  31743  dvnprodlem3  31745  itgioocnicc  31776  iblcncfioo  31777  dirkerper  31878  dirkertrigeq  31883  dirkercncflem2  31886  fourierdlem10  31899  fourierdlem32  31921  fourierdlem33  31922  fourierdlem37  31926  fourierdlem62  31951  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem79  31968  fourierdlem81  31970  fourierdlem82  31971  fourierdlem93  31982  fourierdlem97  31986  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  sqwvfoura  32011  sqwvfourb  32012  fourierswlem  32013  fouriersw  32014  etransclem4  32021  etransclem15  32032  etransclem19  32036  etransclem20  32037  etransclem23  32040  etransclem24  32041  etransclem25  32042  etransclem27  32044  etransclem31  32048  etransclem32  32049  afvfundmfveq  32223  linc1  33026  lincext3  33057  lindslinindsimp1  33058  el0ldep  33067  islindeps2  33084  bj-xpima2sn  34515  cdleme27a  36093  cdleme31sn1  36107  cdleme31fv1  36117  cdlemk40t  36644  dihvalb  36964

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