Theorem iftrue 3878

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 968	. . 3 |- ( ph -> ( x e. A <-> ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) ) )
2	1	abbi2dv 2590	. 2 |- ( ph -> A = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) } )
3		dfif2 3874	. 2 |- if ( ph , A , B ) = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) }
4	2, 3	syl6reqr 2524	1 |- ( ph -> if ( ph , A , B ) = A )

Syntax hints:   -> wi 4   /\ wa 376   = wceq 1452   e. wcel 1904   {cab 2457   ifcif 3872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-if 3873

This theorem is referenced by:  iftruei  3879  iftrued  3880  ifsb  3885  ifbi  3893  ifeq2da  3903  ifclda  3904  ifeqda  3905  elimif  3906  ifbothda  3907  ifid  3909  ifeqor  3916  ifnot  3917  ifan  3918  ifor  3919  2if2  3920  dedth  3923  elimhyp  3930  elimhyp2v  3931  elimhyp3v  3932  elimhyp4v  3933  elimdhyp  3935  keephyp2v  3937  keephyp3v  3938  dfopif  4155  dfopg  4156  somin1  5239  somincom  5240  xpima1  5286  dfiota4  5581  elimdelov  6391  ovif12  6394  tz7.44-1  7142  resixpfo  7578  boxriin  7582  boxcutc  7583  pw2f1olem  7694  unxpdomlem2  7795  unxpdomlem3  7796  ordtypelem1  8051  wemaplem2  8080  unwdomg  8117  ixpiunwdom  8124  cantnfp1lem2  8202  cantnfp1lem3  8203  acndom  8500  dfac12lem2  8592  fin23lem14  8781  axcc2lem  8884  pwfseqlem2  9102  uzin  11215  xrmax1  11493  xrmax2  11494  xrmin1  11495  xrmin2  11496  max1ALT  11504  max0sub  11512  ifle  11513  xmulneg1  11580  fzprval  11882  fztpval  11883  modifeq2int  12186  seqf1olem1  12290  seqf1olem2  12291  bcval2  12528  ccatval1  12773  ccatalpha  12787  swrdccat  12903  swrdccat3a  12904  swrdccat3b  12906  repswswrd  12941  cshword  12947  0csh0  12949  ccatco  12991  sgnn  13234  max0add  13450  absmax  13469  sumrblem  13854  fsumcvg  13855  summolem2a  13858  isum  13862  sumss  13867  sumss2  13869  fsumcvg2  13870  fsumser  13873  fsumsplit  13883  sumsplit  13906  prodrblem  14060  fprodcvg  14061  prodmolem2a  14065  zprod  14068  iprod  14069  iprodn0  14071  prodss  14078  fprodsplit  14097  ruclem2  14361  ruclem3  14362  sadadd2lem2  14503  sadcf  14506  sadc0  14507  sadcp1  14508  sadcaddlem  14510  smupf  14531  smup0  14532  gcd0val  14550  eucalgf  14621  eucalginv  14622  eucalglt  14623  lcmf0val  14671  pc0  14883  pcgcd  14906  pcmptcl  14915  pcmpt  14916  pcmpt2  14917  pcprod  14919  fldivp1  14921  prmreclem2  14940  prmreclem4  14942  1arithlem4  14949  vdwlem6  15015  ramtcl2  15045  ramtcl2OLD  15046  ramcl2  15052  ramcl2OLD  15053  ramub1lem1  15063  prmop1  15075  fvprmselelfz  15081  fvprmselgcd1  15082  ressid2  15255  xpscfv  15546  xpsfrnel  15547  xpsaddlem  15559  xpsvsca  15563  gsumval1  16598  mgm2nsgrplem2  16731  sgrp2nmndlem2  16736  symgextfve  17138  symgfixfolem1  17157  pmtrmvd  17175  pmtrfinv  17180  pmtrprfval  17206  pmtrprfvalrn  17207  frgpuptinv  17499  frgpup2  17504  frgpup3lem  17505  cyggex  17610  gsumzsplit  17638  gsummpt1n0  17675  dprdfid  17728  dmdprdsplitlem  17748  abvtrivd  18146  psrlidm  18704  psrridm  18705  mvrf1  18726  mplmonmul  18765  mplcoe1  18766  mplcoe3  18767  mplcoe5  18769  mplmon2  18793  subrgasclcl  18799  evlslem3  18814  evlslem1  18815  coe1tmfv1  18944  ply1sclid  18958  znf1o  19199  uvcvv1  19424  dmatmul  19599  scmatscmiddistr  19610  1mavmul  19650  mulmarep1gsum2  19676  1marepvmarrepid  19677  mdetdiag  19701  mdetralt2  19711  mdetunilem2  19715  mdetunilem7  19720  mdetunilem8  19721  mdetunilem9  19722  mndifsplit  19738  maducoeval2  19742  madugsum  19745  madurid  19746  gsummatr01lem3  19759  gsummatr01  19761  smadiadetglem2  19774  1elcpmat  19816  decpmatid  19871  chfacfscmulgsum  19961  chfacfpmmulgsum  19965  ptpjpre1  20663  ptbasfi  20673  ptpjopn  20704  isfcls  21102  ptcmplem2  21146  ptcmplem3  21147  tsmssplit  21244  dscmet  21665  dscopn  21666  icccmplem2  21919  iccpnfcnv  22050  xrhmeo  22052  pcohtpylem  22128  pcopt  22131  pcopt2  22132  pcoass  22133  pcorevlem  22135  cmetcaulem  22336  ovolicc1  22547  ioorcl  22608  ioorclOLD  22613  i1f1lem  22726  itg11  22728  itg1addlem2  22734  itg1addlem4  22736  i1fres  22742  itg1climres  22751  mbfi1fseqlem4  22755  mbfi1fseqlem5  22756  mbfi1flim  22760  itg2const2  22778  itg2seq  22779  itg2uba  22780  itg2splitlem  22785  itg2split  22786  itg2monolem1  22787  itg2cnlem1  22798  itg2cnlem2  22799  iblcnlem  22825  iblss  22841  iblss2  22842  itgitg2  22843  itgle  22846  itgss  22848  itgss2  22849  itgss3  22851  itgless  22853  ibladdlem  22856  itgaddlem1  22859  iblabslem  22864  iblabs  22865  iblabsr  22866  iblmulc2  22867  bddmulibl  22875  itggt0  22878  itgcn  22879  limcvallem  22905  ellimc2  22911  limccnp  22925  limccnp2  22926  limcco  22927  dvcobr  22979  dvexp2  22987  elply2  23229  elplyd  23235  ply1termlem  23236  coe1termlem  23291  abelthlem9  23474  logtayl  23684  leibpilem2  23946  leibpi  23947  rlimcnp2  23971  efrlim  23974  igamz  24052  isnsqf  24141  mule1  24154  sqff1o  24188  muinv  24201  chtublem  24218  dchrelbasd  24246  bposlem1  24291  bposlem3  24293  bposlem5  24295  bposlem6  24296  lgsval2lem  24313  lgsneg  24326  lgsdilem  24329  lgsdir2  24335  lgsdir  24337  lgsdi  24339  lgsne0  24340  dchrvmasum2if  24414  dchrvmasumiflem1  24418  rpvmasum2  24429  pntrlog2bndlem4  24497  pntrlog2bndlem5  24498  padicabv  24547  ostth2lem4  24553  axlowdimlem15  25065  ifbieq12d2  28237  elimifd  28238  elim2if  28239  resvid2  28665  fzto1stfv1  28688  xrge0iifcnv  28813  xrge0iifiso  28815  xrge0iifhom  28817  indval2  28910  ind1  28914  sigaclfu2  29017  ddeval1  29130  eulerpartlemb  29274  ballotlemsima  29421  ballotlemrv1  29426  ballotlemsimaOLD  29459  ballotlemrv1OLD  29464  signsw0glem  29514  signswmnd  29518  signswrid  29519  indispcon  30029  mrsubvr  30221  dfrdg2  30513  dfrdg3  30514  unisnif  30763  dfrdg4  30789  fnejoin2  31096  bj-xpima2sn  31621  finxpreclem1  31851  finxpreclem3  31855  poimirlem2  32006  poimirlem15  32019  poimirlem16  32020  poimirlem17  32021  poimirlem19  32023  poimirlem20  32024  poimirlem24  32028  mblfinlem2  32042  mbfposadd  32052  itg2addnclem  32057  itg2gt0cn  32061  ibladdnclem  32062  itgaddnclem1  32064  iblabsnclem  32069  iblabsnc  32070  iblmulc2nc  32071  bddiblnc  32076  itggt0cn  32078  ftc1anclem4  32084  ftc1anclem5  32085  ftc1anclem6  32086  ftc1anclem7  32087  ftc1anclem8  32088  ftc1anc  32089  areacirclem5  32100  areacirc  32101  fdc  32138  heiborlem4  32210  ac6s6  32479  cdleme27a  34005  cdleme31sn1  34019  cdleme31fv1  34029  cdlemk40t  34556  dihvalb  34876  pw2f1ocnv  35963  aomclem5  35987  kelac1  35992  sdrgacs  36138  phisum  36147  mon1pid  36153  arearect  36171  areaquad  36172  refsum2cnlem1  37421  upbdrech2  37614  lptioo2  37808  lptioo1  37809  coskpi2  37838  cosknegpi  37841  cncfiooicclem1  37868  cncfiooiccre  37870  dvnxpaek  37914  dvnprodlem1  37918  dvnprodlem3  37920  itgioocnicc  37951  iblcncfioo  37952  volico  37958  sublevolico  37959  volioore  37965  voliooico  37967  dirkerper  38070  dirkertrigeq  38075  dirkercncflem2  38078  fourierdlem10  38091  fourierdlem32  38114  fourierdlem33  38115  fourierdlem37  38119  fourierdlem62  38144  fourierdlem73  38155  fourierdlem74  38156  fourierdlem75  38157  fourierdlem79  38161  fourierdlem81  38163  fourierdlem82  38164  fourierdlem93  38175  fourierdlem97  38179  fourierdlem101  38183  fourierdlem103  38185  fourierdlem104  38186  sqwvfoura  38204  sqwvfourb  38205  fourierswlem  38206  fouriersw  38207  etransclem4  38215  etransclem15  38226  etransclem19  38230  etransclem20  38231  etransclem23  38234  etransclem24  38235  etransclem25  38236  etransclem27  38238  etransclem31  38242  etransclem32  38243  nnfoctbdjlem  38409  isomenndlem  38470  ovn0val  38490  hoidmv0val  38523  hsphoidmvle2  38525  hoidmv1lelem1  38531  hoidmv1lelem2  38532  hoidmv1le  38534  hoidmvlelem2  38536  hoidmvlelem3  38537  ovnhoilem1  38541  hspdifhsp  38556  hoidifhspdmvle  38560  hspmbllem1  38566  hspmbllem2  38567  hspmbl  38569  volico2  38581  ovnsubadd2lem  38585  ovolval4lem2  38590  ovolval5lem1  38592  afvfundmfveq  38785  pfxccat3a  39117  cshword2  39125  opvtxval  39258  opiedgval  39261  linc1  40726  lincext3  40757  lindslinindsimp1  40758  el0ldep  40767  islindeps2  40784