Theorem iftrue 3906

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 943	. . 3 |- ( ph -> ( x e. A <-> ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) ) )
2	1	abbi2dv 2591	. 2 |- ( ph -> A = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) } )
3		dfif2 3902	. 2 |- if ( ph , A , B ) = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) }
4	2, 3	syl6reqr 2514	1 |- ( ph -> if ( ph , A , B ) = A )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1370   e. wcel 1758   {cab 2439   ifcif 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-if 3901

This theorem is referenced by:  iftruei  3907  ifsb  3911  ifbi  3919  ifeq2da  3929  ifclda  3930  ifeqda  3931  elimif  3932  ifbothda  3933  ifid  3935  ifeqor  3942  ifnot  3943  ifan  3944  ifor  3945  2if2  3946  dedth  3950  elimhyp  3957  elimhyp2v  3958  elimhyp3v  3959  elimhyp4v  3960  elimdhyp  3962  keephyp2v  3964  keephyp3v  3965  dfopif  4165  dfopg  4166  somin1  5343  somincom  5344  xpima1  5390  dfiota4  5518  elimdelov  6277  ovif12  6280  mpt2snif  6295  tz7.44-1  6973  tz7.44-3  6975  resixpfo  7412  boxriin  7416  boxcutc  7417  pw2f1olem  7526  unxpdomlem2  7630  unxpdomlem3  7631  ordtypelem1  7844  wemaplem2  7873  unwdomg  7911  ixpiunwdom  7918  cantnfp1lem2  7999  cantnfp1lem3  8000  cantnfp1lem2OLD  8025  cantnfp1lem3OLD  8026  acndom  8333  iunfictbso  8396  dfac12lem2  8425  fin23lem14  8614  axcc2lem  8717  ttukeylem7  8796  pwfseqlem2  8938  uzin  11005  xrmax1  11259  xrmax2  11260  xrmin1  11261  xrmin2  11262  max1ALT  11270  max0sub  11278  ifle  11279  xmulneg1  11344  xmulpnf1  11349  fzprval  11635  fztpval  11636  modifeq2int  11879  seqf1olem1  11963  seqf1olem2  11964  expnnval  11986  bcval2  12199  ccatval1  12395  lswccat0lsw  12407  swrdval2  12435  swrdlend  12444  swrd0  12446  swrdccat  12503  swrdccat3a  12504  swrdccat3b  12506  swrdccatid  12507  repswswrd  12541  cshword  12547  0csh0  12549  ccatco  12582  sgnn  12702  max0add  12918  absmax  12936  sumeq2ii  13289  sumrblem  13307  fsumcvg  13308  summolem2a  13311  isum  13315  sumss  13320  sumss2  13322  fsumcvg2  13323  fsumser  13326  fsumsplit  13335  sumsplit  13354  ef0lem  13483  rpnnen2lem3  13618  rpnnen2lem9  13624  ruclem2  13633  ruclem3  13634  sadadd2lem2  13765  sadcf  13768  sadc0  13769  sadcp1  13770  sadcaddlem  13772  smupf  13793  smup0  13794  gcd0val  13812  eucalgf  13877  eucalginv  13878  eucalglt  13879  iserodd  14021  pc0  14040  pcgcd  14063  pcmptcl  14072  pcmpt  14073  pcmpt2  14074  pcprod  14076  fldivp1  14078  prmreclem2  14097  prmreclem4  14099  1arithlem4  14106  vdwlem6  14166  ramtcl2  14191  ramcl2  14196  ramub1lem1  14206  ressid2  14346  xpscfv  14620  xpsfrnel  14621  xpsaddlem  14633  xpsvsca  14637  setcepi  15076  gsumval1  15629  gsumval2a  15632  mulgnn  15753  symgextfve  16044  symgfixfolem1  16064  pmtrprfv  16079  pmtrmvd  16082  pmtrfinv  16087  pmtrprfval  16113  pmtrprfvalrn  16114  psgnunilem1  16119  dfod2  16187  oddvds2  16189  frgpuptinv  16390  frgpup2  16395  frgpup3lem  16396  cyggenod  16483  cyggex  16496  gsumzsplit  16540  gsumzsplitOLD  16541  gsummpt1n0  16579  dprdfid  16630  dprdfidOLD  16637  dmdprdsplitlem  16657  dmdprdsplitlemOLD  16658  abvtrivd  17049  psrlidm  17598  psrlidmOLD  17599  psrridm  17600  psrridmOLD  17601  mvrf1  17623  mplmonmul  17668  mplcoe1  17669  mplcoe3  17670  mplcoe3OLD  17671  mplcoe5  17673  mplcoe2OLD  17675  mplmon2  17700  subrgasclcl  17706  evlslem3  17725  evlslem1  17726  coe1tm  17851  coe1tmfv1  17852  coe1tmmul2fv  17856  coe1pwmulfv  17858  coe1sclmul  17860  coe1sclmul2  17862  ply1sclid  17866  znf1o  18110  uvcvv1  18340  1mavmul  18487  mulmarep1gsum2  18513  1marepvmarrepid  18514  m1detdiag  18536  mdetdiag  18538  mdetrsca2  18543  mdetrlin2  18546  mdetralt2  18548  mdetunilem2  18552  mdetunilem5  18555  mdetunilem7  18557  mdetunilem8  18558  mdetunilem9  18559  mndifsplit  18575  maducoeval2  18579  madugsum  18582  madurid  18583  symgmatr01lem  18592  gsummatr01lem3  18596  gsummatr01  18598  smadiadetglem2  18611  2ndcdisj  19193  ptpjpre1  19277  ptbasfi  19287  ptpjopn  19318  isfcls  19715  ptcmplem2  19758  ptcmplem3  19759  tsmssplit  19859  dscmet  20298  dscopn  20299  xrsxmet  20519  icccmplem2  20533  cnmpt2pc  20633  iccpnfcnv  20649  xrhmeo  20651  oprpiece1res1  20656  htpycc  20685  pcoval1  20718  pcohtpylem  20724  pcopt  20727  pcopt2  20728  pcoass  20729  pcorevlem  20731  cmetcaulem  20932  ovolunlem1a  21112  ovolunlem1  21113  ovolicc1  21132  ovolicc2lem3  21135  ovolicc2lem4  21136  ioorcl  21191  i1f1lem  21301  itg11  21303  itg1addlem2  21309  itg1addlem4  21311  i1fres  21317  itg1climres  21326  mbfi1fseqlem4  21330  mbfi1fseqlem5  21331  mbfi1fseqlem6  21332  mbfi1flim  21335  itg2const2  21353  itg2seq  21354  itg2uba  21355  itg2splitlem  21360  itg2split  21361  itg2monolem1  21362  itg2cnlem1  21373  itg2cnlem2  21374  iblcnlem  21400  iblss  21416  iblss2  21417  itgitg2  21418  itgle  21421  itgss  21423  itgss2  21424  itgss3  21426  itgless  21428  ibladdlem  21431  itgaddlem1  21434  iblabslem  21439  iblabs  21440  iblabsr  21441  iblmulc2  21442  itgspliticc  21448  bddmulibl  21450  itggt0  21453  itgcn  21454  ditgpos  21465  limcvallem  21480  ellimc2  21486  limcres  21495  limccnp  21500  limccnp2  21501  limcco  21502  dvcobr  21554  dvexp2  21562  elply2  21798  elplyd  21804  ply1termlem  21805  plyeq0lem  21812  plypf1  21814  coeeq2  21844  coe1termlem  21859  dvply1  21884  aareccl  21926  dvtaylp  21969  pserdvlem2  22027  abelthlem9  22039  logtayl  22239  leibpilem2  22470  leibpi  22471  rlimcnp2  22494  efrlim  22497  isppw  22586  vmappw  22588  muval1  22605  isnsqf  22607  mule1  22620  sqff1o  22654  muinv  22667  chtublem  22684  dchrelbasd  22712  dchr1  22730  dchrptlem2  22738  bposlem1  22757  bposlem3  22759  bposlem5  22761  bposlem6  22762  lgsval2lem  22779  lgsneg  22792  lgsdilem  22795  lgsdir2  22801  lgsdir  22803  lgsdi  22805  lgsne0  22806  rplogsumlem2  22868  dchrvmasum2if  22880  dchrvmasumiflem1  22884  dchrisum0flblem2  22892  dchrisum0fno1  22894  rpvmasum2  22895  rplogsum  22910  pntrlog2bndlem4  22963  pntrlog2bndlem5  22964  padicabv  23013  ostth2lem4  23019  axlowdimlem15  23355  eupath2  23754  gxpval  23899  ifbieq12d2  26056  elimifd  26057  elim2if  26058  partfun  26145  ofldchr  26428  resvid2  26442  xrge0iifcnv  26509  xrge0iifiso  26511  xrge0iifhom  26513  indval2  26617  ind1  26621  esumpinfval  26668  sigaclfu2  26710  ddeval1  26795  eulerpartlemb  26896  eulerpartlemgs2  26908  ballotlemsgt1  27038  ballotlemsel1i  27040  ballotlemsi  27042  ballotlemsima  27043  ballotlemrv1  27048  signsw0glem  27099  signswmnd  27103  signswrid  27104  signsvtn  27130  lgamgulmlem4  27163  igamz  27179  indispcon  27268  cvmliftlem10  27328  prodrblem  27587  fprodcvg  27588  prodmolem2a  27592  zprod  27595  iprod  27596  iprodn0  27598  prodss  27605  fprodsplit  27621  dfrdg2  27754  dfrdg3  27755  unisnif  28101  dfrdg4  28126  mblfinlem2  28578  mbfposadd  28588  itg2addnclem  28592  itg2addnc  28595  itg2gt0cn  28596  ibladdnclem  28597  itgaddnclem1  28599  itgaddnclem2  28600  iblabsnclem  28604  iblabsnc  28605  iblmulc2nc  28606  bddiblnc  28611  itggt0cn  28613  ftc1anclem4  28619  ftc1anclem5  28620  ftc1anclem6  28621  ftc1anclem7  28622  ftc1anclem8  28623  ftc1anc  28624  areacirclem5  28637  areacirc  28638  fnejoin2  28739  sdclem1  28788  fdc  28790  heiborlem4  28862  ac6s6  29133  pw2f1ocnv  29535  aomclem5  29560  kelac1  29565  flcidc  29680  sdrgacs  29707  phisum  29716  mon1pid  29722  arearect  29740  areaquad  29741  refsum2cnlem1  29908  afvfundmfveq  30193  clwlkisclwwlklem2fv1  30593  dmatmul  31056  scmatsubcl  31064  scmatmulcl  31066  linc1  31092  lincext3  31123  lindslinindsimp1  31124  el0ldep  31133  islindeps2  31150  1elcpmat  31205  decpmatid  31258  pmatcollpw3fi1lem1  31274  cpmat1dlem  31322  chfacffsupp  31343  chfacfscmul0  31345  chfacfscmulgsum  31347  chfacfpmmul0  31349  chfacfpmmulgsum  31351  bj-xpima2sn  32783  cdleme27a  34350  cdleme31sn1  34364  cdleme31fv1  34374  cdlemefs27cl  34396  cdlemk40t  34901  dihvalb  35221