Theorem iftrue 3916

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 961	. . 3 |- ( ph -> ( x e. A <-> ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) ) )
2	1	abbi2dv 2560	. 2 |- ( ph -> A = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) } )
3		dfif2 3912	. 2 |- if ( ph , A , B ) = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) }
4	2, 3	syl6reqr 2483	1 |- ( ph -> if ( ph , A , B ) = A )

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1438   e. wcel 1869   {cab 2408   ifcif 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-if 3911

This theorem is referenced by:  iftruei  3917  iftrued  3918  ifsb  3923  ifbi  3931  ifeq2da  3941  ifclda  3942  ifeqda  3943  elimif  3944  ifbothda  3945  ifid  3947  ifeqor  3954  ifnot  3955  ifan  3956  ifor  3957  2if2  3958  dedth  3961  elimhyp  3968  elimhyp2v  3969  elimhyp3v  3970  elimhyp4v  3971  elimdhyp  3973  keephyp2v  3975  keephyp3v  3976  dfopif  4182  dfopg  4183  somin1  5250  somincom  5251  xpima1  5297  dfiota4  5591  elimdelov  6384  ovif12  6387  tz7.44-1  7130  resixpfo  7566  boxriin  7570  boxcutc  7571  pw2f1olem  7680  unxpdomlem2  7781  unxpdomlem3  7782  ordtypelem1  8037  wemaplem2  8066  unwdomg  8103  ixpiunwdom  8110  cantnfp1lem2  8187  cantnfp1lem3  8188  acndom  8484  dfac12lem2  8576  fin23lem14  8765  axcc2lem  8868  pwfseqlem2  9086  uzin  11193  xrmax1  11472  xrmax2  11473  xrmin1  11474  xrmin2  11475  max1ALT  11483  max0sub  11491  ifle  11492  xmulneg1  11557  fzprval  11858  fztpval  11859  modifeq2int  12153  seqf1olem1  12253  seqf1olem2  12254  bcval2  12491  ccatval1  12720  swrdccat  12845  swrdccat3a  12846  swrdccat3b  12848  repswswrd  12883  cshword  12889  0csh0  12891  ccatco  12928  sgnn  13151  max0add  13367  absmax  13386  sumrblem  13770  fsumcvg  13771  summolem2a  13774  isum  13778  sumss  13783  sumss2  13785  fsumcvg2  13786  fsumser  13789  fsumsplit  13799  sumsplit  13822  prodrblem  13976  fprodcvg  13977  prodmolem2a  13981  zprod  13984  iprod  13985  iprodn0  13987  prodss  13994  fprodsplit  14013  ruclem2  14277  ruclem3  14278  sadadd2lem2  14417  sadcf  14420  sadc0  14421  sadcp1  14422  sadcaddlem  14424  smupf  14445  smup0  14446  gcd0val  14464  eucalgf  14535  eucalginv  14536  eucalglt  14537  lcmf0val  14585  pc0  14797  pcgcd  14820  pcmptcl  14829  pcmpt  14830  pcmpt2  14831  pcprod  14833  fldivp1  14835  prmreclem2  14854  prmreclem4  14856  1arithlem4  14863  vdwlem6  14929  ramtcl2  14959  ramtcl2OLD  14960  ramcl2  14966  ramcl2OLD  14967  ramub1lem1  14977  prmop1  14989  fvprmselelfz  14995  fvprmselgcd1  14996  ressid2  15170  xpscfv  15461  xpsfrnel  15462  xpsaddlem  15474  xpsvsca  15478  gsumval1  16513  mgm2nsgrplem2  16646  sgrp2nmndlem2  16651  symgextfve  17053  symgfixfolem1  17072  pmtrmvd  17090  pmtrfinv  17095  pmtrprfval  17121  pmtrprfvalrn  17122  frgpuptinv  17414  frgpup2  17419  frgpup3lem  17420  cyggex  17525  gsumzsplit  17553  gsummpt1n0  17590  dprdfid  17643  dmdprdsplitlem  17663  abvtrivd  18061  psrlidm  18620  psrridm  18621  mvrf1  18642  mplmonmul  18681  mplcoe1  18682  mplcoe3  18683  mplcoe5  18685  mplmon2  18709  subrgasclcl  18715  evlslem3  18730  evlslem1  18731  coe1tmfv1  18860  ply1sclid  18874  znf1o  19114  uvcvv1  19339  dmatmul  19514  scmatscmiddistr  19525  1mavmul  19565  mulmarep1gsum2  19591  1marepvmarrepid  19592  mdetdiag  19616  mdetralt2  19626  mdetunilem2  19630  mdetunilem7  19635  mdetunilem8  19636  mdetunilem9  19637  mndifsplit  19653  maducoeval2  19657  madugsum  19660  madurid  19661  gsummatr01lem3  19674  gsummatr01  19676  smadiadetglem2  19689  1elcpmat  19731  decpmatid  19786  chfacfscmulgsum  19876  chfacfpmmulgsum  19880  ptpjpre1  20578  ptbasfi  20588  ptpjopn  20619  isfcls  21016  ptcmplem2  21060  ptcmplem3  21061  tsmssplit  21158  dscmet  21579  dscopn  21580  icccmplem2  21833  iccpnfcnv  21964  xrhmeo  21966  pcohtpylem  22042  pcopt  22045  pcopt2  22046  pcoass  22047  pcorevlem  22049  cmetcaulem  22250  ovolicc1  22461  ioorcl  22521  ioorclOLD  22526  i1f1lem  22639  itg11  22641  itg1addlem2  22647  itg1addlem4  22649  i1fres  22655  itg1climres  22664  mbfi1fseqlem4  22668  mbfi1fseqlem5  22669  mbfi1flim  22673  itg2const2  22691  itg2seq  22692  itg2uba  22693  itg2splitlem  22698  itg2split  22699  itg2monolem1  22700  itg2cnlem1  22711  itg2cnlem2  22712  iblcnlem  22738  iblss  22754  iblss2  22755  itgitg2  22756  itgle  22759  itgss  22761  itgss2  22762  itgss3  22764  itgless  22766  ibladdlem  22769  itgaddlem1  22772  iblabslem  22777  iblabs  22778  iblabsr  22779  iblmulc2  22780  bddmulibl  22788  itggt0  22791  itgcn  22792  limcvallem  22818  ellimc2  22824  limccnp  22838  limccnp2  22839  limcco  22840  dvcobr  22892  dvexp2  22900  elply2  23142  elplyd  23148  ply1termlem  23149  coe1termlem  23204  abelthlem9  23387  logtayl  23597  leibpilem2  23859  leibpi  23860  rlimcnp2  23884  efrlim  23887  igamz  23965  isnsqf  24054  mule1  24067  sqff1o  24101  muinv  24114  chtublem  24131  dchrelbasd  24159  bposlem1  24204  bposlem3  24206  bposlem5  24208  bposlem6  24209  lgsval2lem  24226  lgsneg  24239  lgsdilem  24242  lgsdir2  24248  lgsdir  24250  lgsdi  24252  lgsne0  24253  dchrvmasum2if  24327  dchrvmasumiflem1  24331  rpvmasum2  24342  pntrlog2bndlem4  24410  pntrlog2bndlem5  24411  padicabv  24460  ostth2lem4  24466  axlowdimlem15  24978  ifbieq12d2  28155  elimifd  28156  elim2if  28157  resvid2  28593  fzto1stfv1  28616  xrge0iifcnv  28741  xrge0iifiso  28743  xrge0iifhom  28745  indval2  28838  ind1  28842  sigaclfu2  28945  ddeval1  29059  eulerpartlemb  29203  ballotlemsima  29350  ballotlemrv1  29355  ballotlemsimaOLD  29388  ballotlemrv1OLD  29393  signsw0glem  29444  signswmnd  29448  signswrid  29449  indispcon  29959  mrsubvr  30151  dfrdg2  30443  dfrdg3  30444  unisnif  30691  dfrdg4  30717  fnejoin2  31024  bj-xpima2sn  31513  finxpreclem1  31739  finxpreclem3  31743  poimirlem2  31900  poimirlem15  31913  poimirlem16  31914  poimirlem17  31915  poimirlem19  31917  poimirlem20  31918  poimirlem24  31922  mblfinlem2  31936  mbfposadd  31946  itg2addnclem  31951  itg2gt0cn  31955  ibladdnclem  31956  itgaddnclem1  31958  iblabsnclem  31963  iblabsnc  31964  iblmulc2nc  31965  bddiblnc  31970  itggt0cn  31972  ftc1anclem4  31978  ftc1anclem5  31979  ftc1anclem6  31980  ftc1anclem7  31981  ftc1anclem8  31982  ftc1anc  31983  areacirclem5  31994  areacirc  31995  fdc  32032  heiborlem4  32104  ac6s6  32373  cdleme27a  33897  cdleme31sn1  33911  cdleme31fv1  33921  cdlemk40t  34448  dihvalb  34768  pw2f1ocnv  35856  aomclem5  35880  kelac1  35885  sdrgacs  36031  phisum  36040  mon1pid  36046  arearect  36064  areaquad  36065  refsum2cnlem1  37263  upbdrech2  37412  lptioo2  37575  lptioo1  37576  coskpi2  37605  cosknegpi  37608  cncfiooicclem1  37635  cncfiooiccre  37637  dvnxpaek  37681  dvnprodlem1  37685  dvnprodlem3  37687  itgioocnicc  37718  iblcncfioo  37719  dirkerper  37822  dirkertrigeq  37827  dirkercncflem2  37830  fourierdlem10  37843  fourierdlem32  37866  fourierdlem33  37867  fourierdlem37  37871  fourierdlem62  37896  fourierdlem73  37907  fourierdlem74  37908  fourierdlem75  37909  fourierdlem79  37913  fourierdlem81  37915  fourierdlem82  37916  fourierdlem93  37927  fourierdlem97  37931  fourierdlem101  37935  fourierdlem103  37937  fourierdlem104  37938  sqwvfoura  37956  sqwvfourb  37957  fourierswlem  37958  fouriersw  37959  etransclem4  37967  etransclem15  37978  etransclem19  37982  etransclem20  37983  etransclem23  37986  etransclem24  37987  etransclem25  37988  etransclem27  37990  etransclem31  37994  etransclem32  37995  nnfoctbdjlem  38116  isomenndlem  38174  volico  38182  ovn0val  38191  afvfundmfveq  38396  pfxccat3a  38726  cshword2  38734  opvtxval  38815  opiedgval  38818  linc1  39562  lincext3  39593  lindslinindsimp1  39594  el0ldep  39603  islindeps2  39620