Theorem iftrue 3932

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 952	. . 3 |- ( ph -> ( x e. A <-> ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) ) )
2	1	abbi2dv 2580	. 2 |- ( ph -> A = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) } )
3		dfif2 3928	. 2 |- if ( ph , A , B ) = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) }
4	2, 3	syl6reqr 2503	1 |- ( ph -> if ( ph , A , B ) = A )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1383   e. wcel 1804   {cab 2428   ifcif 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-if 3927

This theorem is referenced by:  iftruei  3933  iftrued  3934  ifsb  3939  ifbi  3947  ifeq2da  3957  ifclda  3958  ifeqda  3959  elimif  3960  ifbothda  3961  ifid  3963  ifeqor  3970  ifnot  3971  ifan  3972  ifor  3973  2if2  3974  dedth  3978  elimhyp  3985  elimhyp2v  3986  elimhyp3v  3987  elimhyp4v  3988  elimdhyp  3990  keephyp2v  3992  keephyp3v  3993  dfopif  4199  dfopg  4200  somin1  5393  somincom  5394  xpima1  5440  dfiota4  5569  elimdelov  6363  ovif12  6366  tz7.44-1  7074  resixpfo  7509  boxriin  7513  boxcutc  7514  pw2f1olem  7623  unxpdomlem2  7727  unxpdomlem3  7728  ordtypelem1  7946  wemaplem2  7975  unwdomg  8013  ixpiunwdom  8020  cantnfp1lem2  8101  cantnfp1lem3  8102  cantnfp1lem2OLD  8127  cantnfp1lem3OLD  8128  acndom  8435  dfac12lem2  8527  fin23lem14  8716  axcc2lem  8819  pwfseqlem2  9040  uzin  11122  xrmax1  11385  xrmax2  11386  xrmin1  11387  xrmin2  11388  max1ALT  11396  max0sub  11404  ifle  11405  xmulneg1  11470  fzprval  11749  fztpval  11750  modifeq2int  12028  seqf1olem1  12125  seqf1olem2  12126  bcval2  12362  ccatval1  12574  swrdccat  12697  swrdccat3a  12698  swrdccat3b  12700  repswswrd  12735  cshword  12741  0csh0  12743  ccatco  12780  sgnn  12906  max0add  13122  absmax  13141  sumrblem  13512  fsumcvg  13513  summolem2a  13516  isum  13520  sumss  13525  sumss2  13527  fsumcvg2  13528  fsumser  13531  fsumsplit  13541  sumsplit  13562  ruclem2  13842  ruclem3  13843  sadadd2lem2  13977  sadcf  13980  sadc0  13981  sadcp1  13982  sadcaddlem  13984  smupf  14005  smup0  14006  gcd0val  14024  eucalgf  14089  eucalginv  14090  eucalglt  14091  pc0  14255  pcgcd  14278  pcmptcl  14287  pcmpt  14288  pcmpt2  14289  pcprod  14291  fldivp1  14293  prmreclem2  14312  prmreclem4  14314  1arithlem4  14321  vdwlem6  14381  ramtcl2  14406  ramcl2  14411  ramub1lem1  14421  ressid2  14562  xpscfv  14836  xpsfrnel  14837  xpsaddlem  14849  xpsvsca  14853  gsumval1  15778  mgm2nsgrplem2  15911  sgrp2nmndlem2  15916  symgextfve  16318  symgfixfolem1  16337  pmtrmvd  16355  pmtrfinv  16360  pmtrprfval  16386  pmtrprfvalrn  16387  frgpuptinv  16663  frgpup2  16668  frgpup3lem  16669  cyggex  16774  gsumzsplit  16818  gsumzsplitOLD  16819  gsummpt1n0  16866  dprdfid  16931  dprdfidOLD  16938  dmdprdsplitlem  16958  dmdprdsplitlemOLD  16959  abvtrivd  17363  psrlidm  17930  psrlidmOLD  17931  psrridm  17932  psrridmOLD  17933  mvrf1  17955  mplmonmul  18000  mplcoe1  18001  mplcoe3  18002  mplcoe3OLD  18003  mplcoe5  18005  mplcoe2OLD  18007  mplmon2  18032  subrgasclcl  18038  evlslem3  18057  evlslem1  18058  coe1tmfv1  18189  ply1sclid  18203  znf1o  18463  uvcvv1  18693  dmatmul  18872  scmatscmiddistr  18883  1mavmul  18923  mulmarep1gsum2  18949  1marepvmarrepid  18950  mdetdiag  18974  mdetralt2  18984  mdetunilem2  18988  mdetunilem7  18993  mdetunilem8  18994  mdetunilem9  18995  mndifsplit  19011  maducoeval2  19015  madugsum  19018  madurid  19019  gsummatr01lem3  19032  gsummatr01  19034  smadiadetglem2  19047  1elcpmat  19089  decpmatid  19144  chfacfscmulgsum  19234  chfacfpmmulgsum  19238  ptpjpre1  19945  ptbasfi  19955  ptpjopn  19986  isfcls  20383  ptcmplem2  20426  ptcmplem3  20427  tsmssplit  20527  dscmet  20966  dscopn  20967  icccmplem2  21201  iccpnfcnv  21317  xrhmeo  21319  pcohtpylem  21392  pcopt  21395  pcopt2  21396  pcoass  21397  pcorevlem  21399  cmetcaulem  21600  ovolicc1  21800  ioorcl  21859  i1f1lem  21969  itg11  21971  itg1addlem2  21977  itg1addlem4  21979  i1fres  21985  itg1climres  21994  mbfi1fseqlem4  21998  mbfi1fseqlem5  21999  mbfi1flim  22003  itg2const2  22021  itg2seq  22022  itg2uba  22023  itg2splitlem  22028  itg2split  22029  itg2monolem1  22030  itg2cnlem1  22041  itg2cnlem2  22042  iblcnlem  22068  iblss  22084  iblss2  22085  itgitg2  22086  itgle  22089  itgss  22091  itgss2  22092  itgss3  22094  itgless  22096  ibladdlem  22099  itgaddlem1  22102  iblabslem  22107  iblabs  22108  iblabsr  22109  iblmulc2  22110  bddmulibl  22118  itggt0  22121  itgcn  22122  limcvallem  22148  ellimc2  22154  limccnp  22168  limccnp2  22169  limcco  22170  dvcobr  22222  dvexp2  22230  elply2  22466  elplyd  22472  ply1termlem  22473  coe1termlem  22527  abelthlem9  22707  logtayl  22913  leibpilem2  23144  leibpi  23145  rlimcnp2  23168  efrlim  23171  isnsqf  23281  mule1  23294  sqff1o  23328  muinv  23341  chtublem  23358  dchrelbasd  23386  bposlem1  23431  bposlem3  23433  bposlem5  23435  bposlem6  23436  lgsval2lem  23453  lgsneg  23466  lgsdilem  23469  lgsdir2  23475  lgsdir  23477  lgsdi  23479  lgsne0  23480  dchrvmasum2if  23554  dchrvmasumiflem1  23558  rpvmasum2  23569  pntrlog2bndlem4  23637  pntrlog2bndlem5  23638  padicabv  23687  ostth2lem4  23693  axlowdimlem15  24131  ifbieq12d2  27292  elimifd  27293  elim2if  27294  resvid2  27691  xrge0iifcnv  27788  xrge0iifiso  27790  xrge0iifhom  27792  indval2  27901  ind1  27905  sigaclfu2  27994  ddeval1  28079  eulerpartlemb  28180  ballotlemsima  28327  ballotlemrv1  28332  signsw0glem  28383  signswmnd  28387  signswrid  28388  igamz  28463  indispcon  28552  mrsubvr  28744  prodrblem  29036  fprodcvg  29037  prodmolem2a  29041  zprod  29044  iprod  29045  iprodn0  29047  prodss  29054  fprodsplit  29070  dfrdg2  29203  dfrdg3  29204  unisnif  29550  dfrdg4  29575  mblfinlem2  30027  mbfposadd  30037  itg2addnclem  30041  itg2gt0cn  30045  ibladdnclem  30046  itgaddnclem1  30048  iblabsnclem  30053  iblabsnc  30054  iblmulc2nc  30055  bddiblnc  30060  itggt0cn  30062  ftc1anclem4  30068  ftc1anclem5  30069  ftc1anclem6  30070  ftc1anclem7  30071  ftc1anclem8  30072  ftc1anc  30073  areacirclem5  30086  areacirc  30087  fnejoin2  30162  fdc  30213  heiborlem4  30285  ac6s6  30555  pw2f1ocnv  30954  aomclem5  30979  kelac1  30984  sdrgacs  31126  phisum  31135  mon1pid  31141  arearect  31159  areaquad  31160  refsum2cnlem1  31366  upbdrech2  31457  lptioo2  31545  lptioo1  31546  coskpi2  31573  cosknegpi  31576  cncfiooicclem1  31603  cncfiooiccre  31605  itgioocnicc  31666  iblcncfioo  31667  dirkerper  31767  dirkertrigeq  31772  dirkercncflem2  31775  fourierdlem10  31788  fourierdlem32  31810  fourierdlem33  31811  fourierdlem37  31815  fourierdlem62  31840  fourierdlem73  31851  fourierdlem74  31852  fourierdlem75  31853  fourierdlem79  31857  fourierdlem81  31859  fourierdlem82  31860  fourierdlem93  31871  fourierdlem97  31875  fourierdlem101  31879  fourierdlem103  31881  fourierdlem104  31882  sqwvfoura  31900  sqwvfourb  31901  fourierswlem  31902  fouriersw  31903  afvfundmfveq  32061  linc1  32761  lincext3  32792  lindslinindsimp1  32793  el0ldep  32802  islindeps2  32819  bj-xpima2sn  34263  cdleme27a  35833  cdleme31sn1  35847  cdleme31fv1  35857  cdlemk40t  36384  dihvalb  36704