Theorem iftrue 3785

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 936	. . 3 |- ( ph -> ( x e. A <-> ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) ) )
2	1	abbi2dv 2548	. 2 |- ( ph -> A = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) } )
3		dfif2 3781	. 2 |- if ( ph , A , B ) = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) }
4	2, 3	syl6reqr 2484	1 |- ( ph -> if ( ph , A , B ) = A )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1362   e. wcel 1755   {cab 2419   ifcif 3779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-if 3780

This theorem is referenced by:  iftruei  3786  ifsb  3790  ifbi  3798  ifeq2da  3808  ifclda  3809  ifeqda  3810  elimif  3811  ifbothda  3812  ifid  3814  ifeqor  3821  ifnot  3822  ifan  3823  ifor  3824  2if2  3825  dedth  3829  elimhyp  3836  elimhyp2v  3837  elimhyp3v  3838  elimhyp4v  3839  elimdhyp  3841  keephyp2v  3843  keephyp3v  3844  dfopif  4044  dfopg  4045  somin1  5222  somincom  5223  xpima1  5269  dfiota4  5397  elimdelov  6156  ovif12  6159  mpt2snif  6173  tz7.44-1  6848  tz7.44-3  6850  resixpfo  7289  boxriin  7293  boxcutc  7294  pw2f1olem  7403  unxpdomlem2  7506  unxpdomlem3  7507  ordtypelem1  7720  wemaplem2  7749  unwdomg  7787  ixpiunwdom  7794  cantnfp1lem2  7875  cantnfp1lem3  7876  cantnfp1lem2OLD  7901  cantnfp1lem3OLD  7902  acndom  8209  iunfictbso  8272  dfac12lem2  8301  fin23lem14  8490  axcc2lem  8593  ttukeylem7  8672  pwfseqlem2  8814  uzin  10881  xrmax1  11135  xrmax2  11136  xrmin1  11137  xrmin2  11138  max1ALT  11146  max0sub  11154  ifle  11155  xmulneg1  11220  xmulpnf1  11225  fzprval  11501  fztpval  11502  modifeq2int  11745  seqf1olem1  11829  seqf1olem2  11830  expnnval  11852  bcval2  12065  ccatval1  12260  lswccat0lsw  12272  swrdval2  12300  swrdlend  12309  swrd0  12311  swrdccat  12368  swrdccat3a  12369  swrdccat3b  12371  swrdccatid  12372  repswswrd  12406  cshword  12412  0csh0  12414  ccatco  12447  sgnn  12567  max0add  12783  absmax  12801  sumeq2ii  13154  sumrblem  13172  fsumcvg  13173  summolem2a  13176  isum  13180  sumss  13185  sumss2  13187  fsumcvg2  13188  fsumser  13191  fsumsplit  13200  sumsplit  13219  ef0lem  13347  rpnnen2lem3  13482  rpnnen2lem9  13488  ruclem2  13497  ruclem3  13498  sadadd2lem2  13629  sadcf  13632  sadc0  13633  sadcp1  13634  sadcaddlem  13636  smupf  13657  smup0  13658  gcd0val  13676  eucalgf  13741  eucalginv  13742  eucalglt  13743  iserodd  13885  pc0  13904  pcgcd  13927  pcmptcl  13936  pcmpt  13937  pcmpt2  13938  pcprod  13940  fldivp1  13942  prmreclem2  13961  prmreclem4  13963  1arithlem4  13970  vdwlem6  14030  ramtcl2  14055  ramcl2  14060  ramub1lem1  14070  ressid2  14209  xpscfv  14483  xpsfrnel  14484  xpsaddlem  14496  xpsvsca  14500  setcepi  14939  gsumval1  15489  gsumval2a  15492  mulgnn  15613  symgextfve  15904  symgfixfolem1  15924  pmtrprfv  15939  pmtrmvd  15942  pmtrfinv  15947  pmtrprfval  15973  pmtrprfvalrn  15974  psgnunilem1  15979  dfod2  16045  oddvds2  16047  frgpuptinv  16248  frgpup2  16253  frgpup3lem  16254  cyggenod  16341  cyggex  16354  gsumzsplit  16398  gsumzsplitOLD  16399  gsummptif1n0  16431  dprdfid  16481  dprdfidOLD  16488  dmdprdsplitlem  16508  dmdprdsplitlemOLD  16509  abvtrivd  16849  psrlidm  17408  psrlidmOLD  17409  psrridm  17410  psrridmOLD  17411  mvrf1  17432  mplmonmul  17477  mplcoe1  17478  mplcoe3  17479  mplcoe3OLD  17480  mplcoe2  17481  mplcoe2OLD  17482  mplmon2  17507  subrgasclcl  17513  coe1tm  17624  coe1tmfv1  17625  coe1tmmul2fv  17629  coe1pwmulfv  17631  coe1sclmul  17633  coe1sclmul2  17635  ply1sclid  17638  znf1o  17826  uvcvv1  18056  1mavmul  18201  mulmarep1gsum2  18227  1marepvmarrepid  18228  mdet1  18250  mdetrsca2  18253  mdetrlin2  18255  mdetralt2  18257  mdetunilem2  18261  mdetunilem5  18264  mdetunilem7  18266  mdetunilem8  18267  mdetunilem9  18268  mndifsplit  18284  maducoeval2  18288  madugsum  18291  madurid  18292  symgmatr01lem  18301  gsummatr01lem3  18305  gsummatr01  18307  smadiadetglem2  18320  2ndcdisj  18902  ptpjpre1  18986  ptbasfi  18996  ptpjopn  19027  isfcls  19424  ptcmplem2  19467  ptcmplem3  19468  tsmssplit  19568  dscmet  20007  dscopn  20008  xrsxmet  20228  icccmplem2  20242  cnmpt2pc  20342  iccpnfcnv  20358  xrhmeo  20360  oprpiece1res1  20365  htpycc  20394  pcoval1  20427  pcohtpylem  20433  pcopt  20436  pcopt2  20437  pcoass  20438  pcorevlem  20440  cmetcaulem  20641  ovolunlem1a  20821  ovolunlem1  20822  ovolicc1  20841  ovolicc2lem3  20844  ovolicc2lem4  20845  ioorcl  20899  i1f1lem  21009  itg11  21011  itg1addlem2  21017  itg1addlem4  21019  i1fres  21025  itg1climres  21034  mbfi1fseqlem4  21038  mbfi1fseqlem5  21039  mbfi1fseqlem6  21040  mbfi1flim  21043  itg2const2  21061  itg2seq  21062  itg2uba  21063  itg2splitlem  21068  itg2split  21069  itg2monolem1  21070  itg2cnlem1  21081  itg2cnlem2  21082  iblcnlem  21108  iblss  21124  iblss2  21125  itgitg2  21126  itgle  21129  itgss  21131  itgss2  21132  itgss3  21134  itgless  21136  ibladdlem  21139  itgaddlem1  21142  iblabslem  21147  iblabs  21148  iblabsr  21149  iblmulc2  21150  itgspliticc  21156  bddmulibl  21158  itggt0  21161  itgcn  21162  ditgpos  21173  limcvallem  21188  ellimc2  21194  limcres  21203  limccnp  21208  limccnp2  21209  limcco  21210  dvcobr  21262  dvexp2  21270  evlslem3  21366  evlslem1  21367  elply2  21549  elplyd  21555  ply1termlem  21556  plyeq0lem  21563  plypf1  21565  coeeq2  21595  coe1termlem  21610  dvply1  21635  aareccl  21677  dvtaylp  21720  pserdvlem2  21778  abelthlem9  21790  logtayl  21990  leibpilem2  22221  leibpi  22222  rlimcnp2  22245  efrlim  22248  isppw  22337  vmappw  22339  muval1  22356  isnsqf  22358  mule1  22371  sqff1o  22405  muinv  22418  chtublem  22435  dchrelbasd  22463  dchr1  22481  dchrptlem2  22489  bposlem1  22508  bposlem3  22510  bposlem5  22512  bposlem6  22513  lgsval2lem  22530  lgsneg  22543  lgsdilem  22546  lgsdir2  22552  lgsdir  22554  lgsdi  22556  lgsne0  22557  rplogsumlem2  22619  dchrvmasum2if  22631  dchrvmasumiflem1  22635  dchrisum0flblem2  22643  dchrisum0fno1  22645  rpvmasum2  22646  rplogsum  22661  pntrlog2bndlem4  22714  pntrlog2bndlem5  22715  padicabv  22764  ostth2lem4  22770  axlowdimlem15  23025  eupath2  23424  gxpval  23569  ifbieq12d2  25727  elimifd  25729  elim2if  25730  partfun  25817  ofldchr  26135  resvid2  26150  xrge0iifcnv  26217  xrge0iifiso  26219  xrge0iifhom  26221  indval2  26325  ind1  26329  esumpinfval  26376  sigaclfu2  26418  ddeval1  26504  eulerpartlemb  26599  eulerpartlemgs2  26611  ballotlemsgt1  26741  ballotlemsel1i  26743  ballotlemsi  26745  ballotlemsima  26746  ballotlemrv1  26751  signsw0glem  26802  signswmnd  26806  signswrid  26807  signsvtn  26833  lgamgulmlem4  26866  igamz  26882  indispcon  26971  cvmliftlem10  27031  prodrblem  27289  fprodcvg  27290  prodmolem2a  27294  zprod  27297  iprod  27298  iprodn0  27300  prodss  27307  fprodsplit  27323  dfrdg2  27456  dfrdg3  27457  unisnif  27803  dfrdg4  27828  mblfinlem2  28273  mbfposadd  28283  itg2addnclem  28287  itg2addnc  28290  itg2gt0cn  28291  ibladdnclem  28292  itgaddnclem1  28294  itgaddnclem2  28295  iblabsnclem  28299  iblabsnc  28300  iblmulc2nc  28301  bddiblnc  28306  itggt0cn  28308  ftc1anclem4  28314  ftc1anclem5  28315  ftc1anclem6  28316  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  areacirclem5  28332  areacirc  28333  fnejoin2  28434  sdclem1  28483  fdc  28485  heiborlem4  28557  ac6s6  28829  pw2f1ocnv  29231  aomclem5  29256  kelac1  29261  flcidc  29376  sdrgacs  29403  phisum  29412  mon1pid  29418  arearect  29436  areaquad  29437  refsum2cnlem1  29604  afvfundmfveq  29890  clwlkisclwwlklem2fv1  30290  linc1  30668  lincext3  30699  lindslinindsimp1  30700  el0ldep  30709  islindeps2  30726  bj-xpima2sn  32033  cdleme27a  33584  cdleme31sn1  33598  cdleme31fv1  33608  cdlemefs27cl  33630  cdlemk40t  34135  dihvalb  34455