Theorem iftrue 3792

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 2553	. 2 |- ( ph -> A = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) } )
3		dfif2 3788	. 2 |- if ( ph , A , B ) = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) }
4	2, 3	syl6reqr 2489	1 |- ( ph -> if ( ph , A , B ) = A )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   e. wcel 1756   {cab 2424   ifcif 3786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-if 3787

This theorem is referenced by:  iftruei  3793  ifsb  3797  ifbi  3805  ifeq2da  3815  ifclda  3816  ifeqda  3817  elimif  3818  ifbothda  3819  ifid  3821  ifeqor  3828  ifnot  3829  ifan  3830  ifor  3831  2if2  3832  dedth  3836  elimhyp  3843  elimhyp2v  3844  elimhyp3v  3845  elimhyp4v  3846  elimdhyp  3848  keephyp2v  3850  keephyp3v  3851  dfopif  4051  dfopg  4052  somin1  5229  somincom  5230  xpima1  5276  dfiota4  5404  elimdelov  6162  ovif12  6165  mpt2snif  6179  tz7.44-1  6854  tz7.44-3  6856  resixpfo  7293  boxriin  7297  boxcutc  7298  pw2f1olem  7407  unxpdomlem2  7510  unxpdomlem3  7511  ordtypelem1  7724  wemaplem2  7753  unwdomg  7791  ixpiunwdom  7798  cantnfp1lem2  7879  cantnfp1lem3  7880  cantnfp1lem2OLD  7905  cantnfp1lem3OLD  7906  acndom  8213  iunfictbso  8276  dfac12lem2  8305  fin23lem14  8494  axcc2lem  8597  ttukeylem7  8676  pwfseqlem2  8818  uzin  10885  xrmax1  11139  xrmax2  11140  xrmin1  11141  xrmin2  11142  max1ALT  11150  max0sub  11158  ifle  11159  xmulneg1  11224  xmulpnf1  11229  fzprval  11509  fztpval  11510  modifeq2int  11753  seqf1olem1  11837  seqf1olem2  11838  expnnval  11860  bcval2  12073  ccatval1  12268  lswccat0lsw  12280  swrdval2  12308  swrdlend  12317  swrd0  12319  swrdccat  12376  swrdccat3a  12377  swrdccat3b  12379  swrdccatid  12380  repswswrd  12414  cshword  12420  0csh0  12422  ccatco  12455  sgnn  12575  max0add  12791  absmax  12809  sumeq2ii  13162  sumrblem  13180  fsumcvg  13181  summolem2a  13184  isum  13188  sumss  13193  sumss2  13195  fsumcvg2  13196  fsumser  13199  fsumsplit  13208  sumsplit  13227  ef0lem  13356  rpnnen2lem3  13491  rpnnen2lem9  13497  ruclem2  13506  ruclem3  13507  sadadd2lem2  13638  sadcf  13641  sadc0  13642  sadcp1  13643  sadcaddlem  13645  smupf  13666  smup0  13667  gcd0val  13685  eucalgf  13750  eucalginv  13751  eucalglt  13752  iserodd  13894  pc0  13913  pcgcd  13936  pcmptcl  13945  pcmpt  13946  pcmpt2  13947  pcprod  13949  fldivp1  13951  prmreclem2  13970  prmreclem4  13972  1arithlem4  13979  vdwlem6  14039  ramtcl2  14064  ramcl2  14069  ramub1lem1  14079  ressid2  14218  xpscfv  14492  xpsfrnel  14493  xpsaddlem  14505  xpsvsca  14509  setcepi  14948  gsumval1  15500  gsumval2a  15503  mulgnn  15624  symgextfve  15915  symgfixfolem1  15935  pmtrprfv  15950  pmtrmvd  15953  pmtrfinv  15958  pmtrprfval  15984  pmtrprfvalrn  15985  psgnunilem1  15990  dfod2  16056  oddvds2  16058  frgpuptinv  16259  frgpup2  16264  frgpup3lem  16265  cyggenod  16352  cyggex  16365  gsumzsplit  16409  gsumzsplitOLD  16410  gsummptif1n0  16445  dprdfid  16495  dprdfidOLD  16502  dmdprdsplitlem  16522  dmdprdsplitlemOLD  16523  abvtrivd  16903  psrlidm  17451  psrlidmOLD  17452  psrridm  17453  psrridmOLD  17454  mvrf1  17475  mplmonmul  17520  mplcoe1  17521  mplcoe3  17522  mplcoe3OLD  17523  mplcoe2  17524  mplcoe2OLD  17525  mplmon2  17550  subrgasclcl  17556  evlslem3  17575  evlslem1  17576  coe1tm  17701  coe1tmfv1  17702  coe1tmmul2fv  17706  coe1pwmulfv  17708  coe1sclmul  17710  coe1sclmul2  17712  ply1sclid  17715  znf1o  17959  uvcvv1  18189  1mavmul  18334  mulmarep1gsum2  18360  1marepvmarrepid  18361  mdet1  18383  mdetrsca2  18386  mdetrlin2  18388  mdetralt2  18390  mdetunilem2  18394  mdetunilem5  18397  mdetunilem7  18399  mdetunilem8  18400  mdetunilem9  18401  mndifsplit  18417  maducoeval2  18421  madugsum  18424  madurid  18425  symgmatr01lem  18434  gsummatr01lem3  18438  gsummatr01  18440  smadiadetglem2  18453  2ndcdisj  19035  ptpjpre1  19119  ptbasfi  19129  ptpjopn  19160  isfcls  19557  ptcmplem2  19600  ptcmplem3  19601  tsmssplit  19701  dscmet  20140  dscopn  20141  xrsxmet  20361  icccmplem2  20375  cnmpt2pc  20475  iccpnfcnv  20491  xrhmeo  20493  oprpiece1res1  20498  htpycc  20527  pcoval1  20560  pcohtpylem  20566  pcopt  20569  pcopt2  20570  pcoass  20571  pcorevlem  20573  cmetcaulem  20774  ovolunlem1a  20954  ovolunlem1  20955  ovolicc1  20974  ovolicc2lem3  20977  ovolicc2lem4  20978  ioorcl  21032  i1f1lem  21142  itg11  21144  itg1addlem2  21150  itg1addlem4  21152  i1fres  21158  itg1climres  21167  mbfi1fseqlem4  21171  mbfi1fseqlem5  21172  mbfi1fseqlem6  21173  mbfi1flim  21176  itg2const2  21194  itg2seq  21195  itg2uba  21196  itg2splitlem  21201  itg2split  21202  itg2monolem1  21203  itg2cnlem1  21214  itg2cnlem2  21215  iblcnlem  21241  iblss  21257  iblss2  21258  itgitg2  21259  itgle  21262  itgss  21264  itgss2  21265  itgss3  21267  itgless  21269  ibladdlem  21272  itgaddlem1  21275  iblabslem  21280  iblabs  21281  iblabsr  21282  iblmulc2  21283  itgspliticc  21289  bddmulibl  21291  itggt0  21294  itgcn  21295  ditgpos  21306  limcvallem  21321  ellimc2  21327  limcres  21336  limccnp  21341  limccnp2  21342  limcco  21343  dvcobr  21395  dvexp2  21403  elply2  21639  elplyd  21645  ply1termlem  21646  plyeq0lem  21653  plypf1  21655  coeeq2  21685  coe1termlem  21700  dvply1  21725  aareccl  21767  dvtaylp  21810  pserdvlem2  21868  abelthlem9  21880  logtayl  22080  leibpilem2  22311  leibpi  22312  rlimcnp2  22335  efrlim  22338  isppw  22427  vmappw  22429  muval1  22446  isnsqf  22448  mule1  22461  sqff1o  22495  muinv  22508  chtublem  22525  dchrelbasd  22553  dchr1  22571  dchrptlem2  22579  bposlem1  22598  bposlem3  22600  bposlem5  22602  bposlem6  22603  lgsval2lem  22620  lgsneg  22633  lgsdilem  22636  lgsdir2  22642  lgsdir  22644  lgsdi  22646  lgsne0  22647  rplogsumlem2  22709  dchrvmasum2if  22721  dchrvmasumiflem1  22725  dchrisum0flblem2  22733  dchrisum0fno1  22735  rpvmasum2  22736  rplogsum  22751  pntrlog2bndlem4  22804  pntrlog2bndlem5  22805  padicabv  22854  ostth2lem4  22860  axlowdimlem15  23153  eupath2  23552  gxpval  23697  ifbieq12d2  25854  elimifd  25856  elim2if  25857  partfun  25944  ofldchr  26233  resvid2  26248  xrge0iifcnv  26315  xrge0iifiso  26317  xrge0iifhom  26319  indval2  26423  ind1  26427  esumpinfval  26474  sigaclfu2  26516  ddeval1  26602  eulerpartlemb  26703  eulerpartlemgs2  26715  ballotlemsgt1  26845  ballotlemsel1i  26847  ballotlemsi  26849  ballotlemsima  26850  ballotlemrv1  26855  signsw0glem  26906  signswmnd  26910  signswrid  26911  signsvtn  26937  lgamgulmlem4  26970  igamz  26986  indispcon  27075  cvmliftlem10  27135  prodrblem  27393  fprodcvg  27394  prodmolem2a  27398  zprod  27401  iprod  27402  iprodn0  27404  prodss  27411  fprodsplit  27427  dfrdg2  27560  dfrdg3  27561  unisnif  27907  dfrdg4  27932  mblfinlem2  28382  mbfposadd  28392  itg2addnclem  28396  itg2addnc  28399  itg2gt0cn  28400  ibladdnclem  28401  itgaddnclem1  28403  itgaddnclem2  28404  iblabsnclem  28408  iblabsnc  28409  iblmulc2nc  28410  bddiblnc  28415  itggt0cn  28417  ftc1anclem4  28423  ftc1anclem5  28424  ftc1anclem6  28425  ftc1anclem7  28426  ftc1anclem8  28427  ftc1anc  28428  areacirclem5  28441  areacirc  28442  fnejoin2  28543  sdclem1  28592  fdc  28594  heiborlem4  28666  ac6s6  28937  pw2f1ocnv  29339  aomclem5  29364  kelac1  29369  flcidc  29484  sdrgacs  29511  phisum  29520  mon1pid  29526  arearect  29544  areaquad  29545  refsum2cnlem1  29712  afvfundmfveq  29997  clwlkisclwwlklem2fv1  30397  dmatmul  30799  scmatsubcl  30807  scmatmulcl  30809  m1detdiag  30823  mdetdiag  30825  linc1  30848  lincext3  30879  lindslinindsimp1  30880  el0ldep  30889  islindeps2  30906  bj-xpima2sn  32297  cdleme27a  33851  cdleme31sn1  33865  cdleme31fv1  33875  cdlemefs27cl  33897  cdlemk40t  34402  dihvalb  34722