Theorem iftrue 3945

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	|- ( ph -> if ( ph , A , B ) = A )

Proof of Theorem iftrue

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dedlem0a 950	. . 3 |- ( ph -> ( x e. A <-> ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) ) )
2	1	abbi2dv 2604	. 2 |- ( ph -> A = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) } )
3		dfif2 3941	. 2 |- if ( ph , A , B ) = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) }
4	2, 3	syl6reqr 2527	1 |- ( ph -> if ( ph , A , B ) = A )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1379   e. wcel 1767   {cab 2452   ifcif 3939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3940

This theorem is referenced by:  iftruei  3946  iftrued  3947  ifsb  3952  ifbi  3960  ifeq2da  3970  ifclda  3971  ifeqda  3972  elimif  3973  ifbothda  3974  ifid  3976  ifeqor  3983  ifnot  3984  ifan  3985  ifor  3986  2if2  3987  dedth  3991  elimhyp  3998  elimhyp2v  3999  elimhyp3v  4000  elimhyp4v  4001  elimdhyp  4003  keephyp2v  4005  keephyp3v  4006  dfopif  4210  dfopg  4211  somin1  5401  somincom  5402  xpima1  5448  dfiota4  5577  elimdelov  6360  ovif12  6363  mpt2snif  6378  tz7.44-1  7069  tz7.44-3  7071  resixpfo  7504  boxriin  7508  boxcutc  7509  pw2f1olem  7618  unxpdomlem2  7722  unxpdomlem3  7723  ordtypelem1  7939  wemaplem2  7968  unwdomg  8006  ixpiunwdom  8013  cantnfp1lem2  8094  cantnfp1lem3  8095  cantnfp1lem2OLD  8120  cantnfp1lem3OLD  8121  acndom  8428  iunfictbso  8491  dfac12lem2  8520  fin23lem14  8709  axcc2lem  8812  ttukeylem7  8891  pwfseqlem2  9033  uzin  11110  xrmax1  11372  xrmax2  11373  xrmin1  11374  xrmin2  11375  max1ALT  11383  max0sub  11391  ifle  11392  xmulneg1  11457  xmulpnf1  11462  fzprval  11736  fztpval  11737  modifeq2int  12013  seqf1olem1  12110  seqf1olem2  12111  expnnval  12133  bcval2  12347  ccatval1  12556  lswccat0lsw  12568  swrdval2  12606  swrdlend  12615  swrd0  12617  swrdccat  12677  swrdccat3a  12678  swrdccat3b  12680  swrdccatid  12681  repswswrd  12715  cshword  12721  0csh0  12723  ccatco  12760  sgnn  12886  max0add  13102  absmax  13121  sumeq2ii  13474  sumrblem  13492  fsumcvg  13493  summolem2a  13496  isum  13500  sumss  13505  sumss2  13507  fsumcvg2  13508  fsumser  13511  fsumsplit  13521  sumsplit  13542  ef0lem  13672  rpnnen2lem3  13807  rpnnen2lem9  13813  ruclem2  13822  ruclem3  13823  sadadd2lem2  13955  sadcf  13958  sadc0  13959  sadcp1  13960  sadcaddlem  13962  smupf  13983  smup0  13984  gcd0val  14002  eucalgf  14067  eucalginv  14068  eucalglt  14069  iserodd  14214  pc0  14233  pcgcd  14256  pcmptcl  14265  pcmpt  14266  pcmpt2  14267  pcprod  14269  fldivp1  14271  prmreclem2  14290  prmreclem4  14292  1arithlem4  14299  vdwlem6  14359  ramtcl2  14384  ramcl2  14389  ramub1lem1  14399  ressid2  14539  xpscfv  14813  xpsfrnel  14814  xpsaddlem  14826  xpsvsca  14830  setcepi  15269  gsumval1  15822  gsumval2a  15825  mulgnn  15948  symgextfve  16239  symgfixfolem1  16259  pmtrprfv  16274  pmtrmvd  16277  pmtrfinv  16282  pmtrprfval  16308  pmtrprfvalrn  16309  psgnunilem1  16314  dfod2  16382  oddvds2  16384  frgpuptinv  16585  frgpup2  16590  frgpup3lem  16591  cyggenod  16678  cyggex  16691  gsumzsplit  16735  gsumzsplitOLD  16736  gsummpt1n0  16783  dprdfid  16847  dprdfidOLD  16854  dmdprdsplitlem  16874  dmdprdsplitlemOLD  16875  abvtrivd  17272  psrlidm  17827  psrlidmOLD  17828  psrridm  17829  psrridmOLD  17830  mvrf1  17852  mplmonmul  17897  mplcoe1  17898  mplcoe3  17899  mplcoe3OLD  17900  mplcoe5  17902  mplcoe2OLD  17904  mplmon2  17929  subrgasclcl  17935  evlslem3  17954  evlslem1  17955  coe1tm  18085  coe1tmfv1  18086  coe1tmmul2fv  18090  coe1pwmulfv  18092  coe1sclmul  18094  coe1sclmul2  18096  ply1sclid  18100  znf1o  18357  uvcvv1  18587  dmatmul  18766  scmatscmiddistr  18777  1mavmul  18817  mulmarep1gsum2  18843  1marepvmarrepid  18844  m1detdiag  18866  mdetdiag  18868  mdetrsca2  18873  mdetrlin2  18876  mdetralt2  18878  mdetunilem2  18882  mdetunilem5  18885  mdetunilem7  18887  mdetunilem8  18888  mdetunilem9  18889  mndifsplit  18905  maducoeval2  18909  madugsum  18912  madurid  18913  symgmatr01lem  18922  gsummatr01lem3  18926  gsummatr01  18928  smadiadetglem2  18941  1elcpmat  18983  decpmatid  19038  pmatcollpw3fi1lem1  19054  chpmat1dlem  19103  chfacfscmul0  19126  chfacfscmulgsum  19128  chfacfpmmul0  19130  chfacfpmmulgsum  19132  2ndcdisj  19723  ptpjpre1  19807  ptbasfi  19817  ptpjopn  19848  isfcls  20245  ptcmplem2  20288  ptcmplem3  20289  tsmssplit  20389  dscmet  20828  dscopn  20829  xrsxmet  21049  icccmplem2  21063  cnmpt2pc  21163  iccpnfcnv  21179  xrhmeo  21181  oprpiece1res1  21186  htpycc  21215  pcoval1  21248  pcohtpylem  21254  pcopt  21257  pcopt2  21258  pcoass  21259  pcorevlem  21261  cmetcaulem  21462  ovolunlem1a  21642  ovolunlem1  21643  ovolicc1  21662  ovolicc2lem3  21665  ovolicc2lem4  21666  ioorcl  21721  i1f1lem  21831  itg11  21833  itg1addlem2  21839  itg1addlem4  21841  i1fres  21847  itg1climres  21856  mbfi1fseqlem4  21860  mbfi1fseqlem5  21861  mbfi1fseqlem6  21862  mbfi1flim  21865  itg2const2  21883  itg2seq  21884  itg2uba  21885  itg2splitlem  21890  itg2split  21891  itg2monolem1  21892  itg2cnlem1  21903  itg2cnlem2  21904  iblcnlem  21930  iblss  21946  iblss2  21947  itgitg2  21948  itgle  21951  itgss  21953  itgss2  21954  itgss3  21956  itgless  21958  ibladdlem  21961  itgaddlem1  21964  iblabslem  21969  iblabs  21970  iblabsr  21971  iblmulc2  21972  itgspliticc  21978  bddmulibl  21980  itggt0  21983  itgcn  21984  ditgpos  21995  limcvallem  22010  ellimc2  22016  limcres  22025  limccnp  22030  limccnp2  22031  limcco  22032  dvcobr  22084  dvexp2  22092  elply2  22328  elplyd  22334  ply1termlem  22335  plyeq0lem  22342  plypf1  22344  coeeq2  22374  coe1termlem  22389  dvply1  22414  aareccl  22456  dvtaylp  22499  pserdvlem2  22557  abelthlem9  22569  logtayl  22769  leibpilem2  23000  leibpi  23001  rlimcnp2  23024  efrlim  23027  isppw  23116  vmappw  23118  muval1  23135  isnsqf  23137  mule1  23150  sqff1o  23184  muinv  23197  chtublem  23214  dchrelbasd  23242  dchr1  23260  dchrptlem2  23268  bposlem1  23287  bposlem3  23289  bposlem5  23291  bposlem6  23292  lgsval2lem  23309  lgsneg  23322  lgsdilem  23325  lgsdir2  23331  lgsdir  23333  lgsdi  23335  lgsne0  23336  rplogsumlem2  23398  dchrvmasum2if  23410  dchrvmasumiflem1  23414  dchrisum0flblem2  23422  dchrisum0fno1  23424  rpvmasum2  23425  rplogsum  23440  pntrlog2bndlem4  23493  pntrlog2bndlem5  23494  padicabv  23543  ostth2lem4  23549  axlowdimlem15  23935  clwlkisclwwlklem2fv1  24458  eupath2  24656  gxpval  24937  ifbieq12d2  27094  elimifd  27095  elim2if  27096  partfun  27188  ofldchr  27467  resvid2  27481  xrge0iifcnv  27551  xrge0iifiso  27553  xrge0iifhom  27555  indval2  27668  ind1  27672  esumpinfval  27719  sigaclfu2  27761  ddeval1  27846  eulerpartlemb  27947  eulerpartlemgs2  27959  ballotlemsgt1  28089  ballotlemsel1i  28091  ballotlemsi  28093  ballotlemsima  28094  ballotlemrv1  28099  signsw0glem  28150  signswmnd  28154  signswrid  28155  signsvtn  28181  lgamgulmlem4  28214  igamz  28230  indispcon  28319  cvmliftlem10  28379  prodrblem  28638  fprodcvg  28639  prodmolem2a  28643  zprod  28646  iprod  28647  iprodn0  28649  prodss  28656  fprodsplit  28672  dfrdg2  28805  dfrdg3  28806  unisnif  29152  dfrdg4  29177  mblfinlem2  29629  mbfposadd  29639  itg2addnclem  29643  itg2addnc  29646  itg2gt0cn  29647  ibladdnclem  29648  itgaddnclem1  29650  itgaddnclem2  29651  iblabsnclem  29655  iblabsnc  29656  iblmulc2nc  29657  bddiblnc  29662  itggt0cn  29664  ftc1anclem4  29670  ftc1anclem5  29671  ftc1anclem6  29672  ftc1anclem7  29673  ftc1anclem8  29674  ftc1anc  29675  areacirclem5  29688  areacirc  29689  fnejoin2  29790  sdclem1  29839  fdc  29841  heiborlem4  29913  ac6s6  30184  pw2f1ocnv  30583  aomclem5  30608  kelac1  30613  flcidc  30728  sdrgacs  30755  phisum  30764  mon1pid  30770  arearect  30788  areaquad  30789  refsum2cnlem1  30990  ifeq123d  31014  upbdrech2  31085  ioondisj2  31089  ioondisj1  31090  lptioo2  31173  lptioo1  31174  coskpi2  31202  cosknegpi  31205  icccncfext  31226  cncfiooicclem1  31232  cncfiooicc  31233  cncfiooiccre  31234  ditgeq3d  31282  itgsubsticclem  31293  itgioocnicc  31295  iblcncfioo  31296  dirkerper  31396  dirkertrigeq  31401  dirkercncflem2  31404  fourierdlem9  31416  fourierdlem10  31417  fourierdlem17  31424  fourierdlem32  31439  fourierdlem33  31440  fourierdlem37  31444  fourierdlem43  31450  fourierdlem62  31469  fourierdlem65  31472  fourierdlem73  31480  fourierdlem74  31481  fourierdlem75  31482  fourierdlem76  31483  fourierdlem79  31486  fourierdlem81  31488  fourierdlem82  31489  fourierdlem89  31496  fourierdlem91  31498  fourierdlem93  31500  fourierdlem97  31504  fourierdlem101  31508  fourierdlem103  31510  fourierdlem104  31511  sqwvfoura  31529  sqwvfourb  31530  fourierswlem  31531  fouriersw  31532  afvfundmfveq  31690  linc1  32099  lincext3  32130  lindslinindsimp1  32131  el0ldep  32140  islindeps2  32157  bj-xpima2sn  33596  cdleme27a  35163  cdleme31sn1  35177  cdleme31fv1  35187  cdlemefs27cl  35209  cdlemk40t  35714  dihvalb  36034