Theorem iftrue 3887

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 963	. . 3 |- ( ph -> ( x e. A <-> ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) ) )
2	1	abbi2dv 2570	. 2 |- ( ph -> A = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) } )
3		dfif2 3883	. 2 |- if ( ph , A , B ) = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) }
4	2, 3	syl6reqr 2504	1 |- ( ph -> if ( ph , A , B ) = A )

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1444   e. wcel 1887   {cab 2437   ifcif 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-if 3882

This theorem is referenced by:  iftruei  3888  iftrued  3889  ifsb  3894  ifbi  3902  ifeq2da  3912  ifclda  3913  ifeqda  3914  elimif  3915  ifbothda  3916  ifid  3918  ifeqor  3925  ifnot  3926  ifan  3927  ifor  3928  2if2  3929  dedth  3932  elimhyp  3939  elimhyp2v  3940  elimhyp3v  3941  elimhyp4v  3942  elimdhyp  3944  keephyp2v  3946  keephyp3v  3947  dfopif  4163  dfopg  4164  somin1  5233  somincom  5234  xpima1  5280  dfiota4  5574  elimdelov  6372  ovif12  6375  tz7.44-1  7124  resixpfo  7560  boxriin  7564  boxcutc  7565  pw2f1olem  7676  unxpdomlem2  7777  unxpdomlem3  7778  ordtypelem1  8033  wemaplem2  8062  unwdomg  8099  ixpiunwdom  8106  cantnfp1lem2  8184  cantnfp1lem3  8185  acndom  8482  dfac12lem2  8574  fin23lem14  8763  axcc2lem  8866  pwfseqlem2  9084  uzin  11191  xrmax1  11470  xrmax2  11471  xrmin1  11472  xrmin2  11473  max1ALT  11481  max0sub  11489  ifle  11490  xmulneg1  11555  fzprval  11856  fztpval  11857  modifeq2int  12152  seqf1olem1  12252  seqf1olem2  12253  bcval2  12490  ccatval1  12722  swrdccat  12849  swrdccat3a  12850  swrdccat3b  12852  repswswrd  12887  cshword  12893  0csh0  12895  ccatco  12932  sgnn  13157  max0add  13373  absmax  13392  sumrblem  13777  fsumcvg  13778  summolem2a  13781  isum  13785  sumss  13790  sumss2  13792  fsumcvg2  13793  fsumser  13796  fsumsplit  13806  sumsplit  13829  prodrblem  13983  fprodcvg  13984  prodmolem2a  13988  zprod  13991  iprod  13992  iprodn0  13994  prodss  14001  fprodsplit  14020  ruclem2  14284  ruclem3  14285  sadadd2lem2  14424  sadcf  14427  sadc0  14428  sadcp1  14429  sadcaddlem  14431  smupf  14452  smup0  14453  gcd0val  14471  eucalgf  14542  eucalginv  14543  eucalglt  14544  lcmf0val  14592  pc0  14804  pcgcd  14827  pcmptcl  14836  pcmpt  14837  pcmpt2  14838  pcprod  14840  fldivp1  14842  prmreclem2  14861  prmreclem4  14863  1arithlem4  14870  vdwlem6  14936  ramtcl2  14966  ramtcl2OLD  14967  ramcl2  14973  ramcl2OLD  14974  ramub1lem1  14984  prmop1  14996  fvprmselelfz  15002  fvprmselgcd1  15003  ressid2  15177  xpscfv  15468  xpsfrnel  15469  xpsaddlem  15481  xpsvsca  15485  gsumval1  16520  mgm2nsgrplem2  16653  sgrp2nmndlem2  16658  symgextfve  17060  symgfixfolem1  17079  pmtrmvd  17097  pmtrfinv  17102  pmtrprfval  17128  pmtrprfvalrn  17129  frgpuptinv  17421  frgpup2  17426  frgpup3lem  17427  cyggex  17532  gsumzsplit  17560  gsummpt1n0  17597  dprdfid  17650  dmdprdsplitlem  17670  abvtrivd  18068  psrlidm  18627  psrridm  18628  mvrf1  18649  mplmonmul  18688  mplcoe1  18689  mplcoe3  18690  mplcoe5  18692  mplmon2  18716  subrgasclcl  18722  evlslem3  18737  evlslem1  18738  coe1tmfv1  18867  ply1sclid  18881  znf1o  19122  uvcvv1  19347  dmatmul  19522  scmatscmiddistr  19533  1mavmul  19573  mulmarep1gsum2  19599  1marepvmarrepid  19600  mdetdiag  19624  mdetralt2  19634  mdetunilem2  19638  mdetunilem7  19643  mdetunilem8  19644  mdetunilem9  19645  mndifsplit  19661  maducoeval2  19665  madugsum  19668  madurid  19669  gsummatr01lem3  19682  gsummatr01  19684  smadiadetglem2  19697  1elcpmat  19739  decpmatid  19794  chfacfscmulgsum  19884  chfacfpmmulgsum  19888  ptpjpre1  20586  ptbasfi  20596  ptpjopn  20627  isfcls  21024  ptcmplem2  21068  ptcmplem3  21069  tsmssplit  21166  dscmet  21587  dscopn  21588  icccmplem2  21841  iccpnfcnv  21972  xrhmeo  21974  pcohtpylem  22050  pcopt  22053  pcopt2  22054  pcoass  22055  pcorevlem  22057  cmetcaulem  22258  ovolicc1  22469  ioorcl  22529  ioorclOLD  22534  i1f1lem  22647  itg11  22649  itg1addlem2  22655  itg1addlem4  22657  i1fres  22663  itg1climres  22672  mbfi1fseqlem4  22676  mbfi1fseqlem5  22677  mbfi1flim  22681  itg2const2  22699  itg2seq  22700  itg2uba  22701  itg2splitlem  22706  itg2split  22707  itg2monolem1  22708  itg2cnlem1  22719  itg2cnlem2  22720  iblcnlem  22746  iblss  22762  iblss2  22763  itgitg2  22764  itgle  22767  itgss  22769  itgss2  22770  itgss3  22772  itgless  22774  ibladdlem  22777  itgaddlem1  22780  iblabslem  22785  iblabs  22786  iblabsr  22787  iblmulc2  22788  bddmulibl  22796  itggt0  22799  itgcn  22800  limcvallem  22826  ellimc2  22832  limccnp  22846  limccnp2  22847  limcco  22848  dvcobr  22900  dvexp2  22908  elply2  23150  elplyd  23156  ply1termlem  23157  coe1termlem  23212  abelthlem9  23395  logtayl  23605  leibpilem2  23867  leibpi  23868  rlimcnp2  23892  efrlim  23895  igamz  23973  isnsqf  24062  mule1  24075  sqff1o  24109  muinv  24122  chtublem  24139  dchrelbasd  24167  bposlem1  24212  bposlem3  24214  bposlem5  24216  bposlem6  24217  lgsval2lem  24234  lgsneg  24247  lgsdilem  24250  lgsdir2  24256  lgsdir  24258  lgsdi  24260  lgsne0  24261  dchrvmasum2if  24335  dchrvmasumiflem1  24339  rpvmasum2  24350  pntrlog2bndlem4  24418  pntrlog2bndlem5  24419  padicabv  24468  ostth2lem4  24474  axlowdimlem15  24986  ifbieq12d2  28159  elimifd  28160  elim2if  28161  resvid2  28591  fzto1stfv1  28614  xrge0iifcnv  28739  xrge0iifiso  28741  xrge0iifhom  28743  indval2  28836  ind1  28840  sigaclfu2  28943  ddeval1  29057  eulerpartlemb  29201  ballotlemsima  29348  ballotlemrv1  29353  ballotlemsimaOLD  29386  ballotlemrv1OLD  29391  signsw0glem  29442  signswmnd  29446  signswrid  29447  indispcon  29957  mrsubvr  30149  dfrdg2  30442  dfrdg3  30443  unisnif  30692  dfrdg4  30718  fnejoin2  31025  bj-xpima2sn  31551  finxpreclem1  31781  finxpreclem3  31785  poimirlem2  31942  poimirlem15  31955  poimirlem16  31956  poimirlem17  31957  poimirlem19  31959  poimirlem20  31960  poimirlem24  31964  mblfinlem2  31978  mbfposadd  31988  itg2addnclem  31993  itg2gt0cn  31997  ibladdnclem  31998  itgaddnclem1  32000  iblabsnclem  32005  iblabsnc  32006  iblmulc2nc  32007  bddiblnc  32012  itggt0cn  32014  ftc1anclem4  32020  ftc1anclem5  32021  ftc1anclem6  32022  ftc1anclem7  32023  ftc1anclem8  32024  ftc1anc  32025  areacirclem5  32036  areacirc  32037  fdc  32074  heiborlem4  32146  ac6s6  32415  cdleme27a  33934  cdleme31sn1  33948  cdleme31fv1  33958  cdlemk40t  34485  dihvalb  34805  pw2f1ocnv  35892  aomclem5  35916  kelac1  35921  sdrgacs  36067  phisum  36076  mon1pid  36082  arearect  36100  areaquad  36101  refsum2cnlem1  37358  upbdrech2  37526  lptioo2  37711  lptioo1  37712  coskpi2  37741  cosknegpi  37744  cncfiooicclem1  37771  cncfiooiccre  37773  dvnxpaek  37817  dvnprodlem1  37821  dvnprodlem3  37823  itgioocnicc  37854  iblcncfioo  37855  dirkerper  37958  dirkertrigeq  37963  dirkercncflem2  37966  fourierdlem10  37979  fourierdlem32  38002  fourierdlem33  38003  fourierdlem37  38007  fourierdlem62  38032  fourierdlem73  38043  fourierdlem74  38044  fourierdlem75  38045  fourierdlem79  38049  fourierdlem81  38051  fourierdlem82  38052  fourierdlem93  38063  fourierdlem97  38067  fourierdlem101  38071  fourierdlem103  38073  fourierdlem104  38074  sqwvfoura  38092  sqwvfourb  38093  fourierswlem  38094  fouriersw  38095  etransclem4  38103  etransclem15  38114  etransclem19  38118  etransclem20  38119  etransclem23  38122  etransclem24  38123  etransclem25  38124  etransclem27  38126  etransclem31  38130  etransclem32  38131  nnfoctbdjlem  38293  isomenndlem  38351  volico  38363  ovn0val  38372  hoidmv0val  38405  hsphoidmvle2  38407  hoidmv1lelem1  38413  hoidmv1lelem2  38414  hoidmv1le  38416  hoidmvlelem2  38418  hoidmvlelem3  38419  ovnhoilem1  38423  hspdifhsp  38438  hoidifhspdmvle  38442  hspmbllem1  38448  hspmbllem2  38449  hspmbl  38451  afvfundmfveq  38640  pfxccat3a  38970  cshword2  38978  opvtxval  39107  opiedgval  39110  linc1  40271  lincext3  40302  lindslinindsimp1  40303  el0ldep  40312  islindeps2  40329