Theorem iftrue 3891

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 953	. . 3 |- ( ph -> ( x e. A <-> ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) ) )
2	1	abbi2dv 2539	. 2 |- ( ph -> A = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) } )
3		dfif2 3887	. 2 |- if ( ph , A , B ) = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) }
4	2, 3	syl6reqr 2462	1 |- ( ph -> if ( ph , A , B ) = A )

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1405   e. wcel 1842   {cab 2387   ifcif 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-if 3886

This theorem is referenced by:  iftruei  3892  iftrued  3893  ifsb  3898  ifbi  3906  ifeq2da  3916  ifclda  3917  ifeqda  3918  elimif  3919  ifbothda  3920  ifid  3922  ifeqor  3929  ifnot  3930  ifan  3931  ifor  3932  2if2  3933  dedth  3936  elimhyp  3943  elimhyp2v  3944  elimhyp3v  3945  elimhyp4v  3946  elimdhyp  3948  keephyp2v  3950  keephyp3v  3951  dfopif  4156  dfopg  4157  somin1  5221  somincom  5222  xpima1  5268  dfiota4  5561  elimdelov  6359  ovif12  6362  tz7.44-1  7109  resixpfo  7545  boxriin  7549  boxcutc  7550  pw2f1olem  7659  unxpdomlem2  7760  unxpdomlem3  7761  ordtypelem1  7977  wemaplem2  8006  unwdomg  8044  ixpiunwdom  8051  cantnfp1lem2  8130  cantnfp1lem3  8131  cantnfp1lem2OLD  8156  cantnfp1lem3OLD  8157  acndom  8464  dfac12lem2  8556  fin23lem14  8745  axcc2lem  8848  pwfseqlem2  9067  uzin  11159  xrmax1  11429  xrmax2  11430  xrmin1  11431  xrmin2  11432  max1ALT  11440  max0sub  11448  ifle  11449  xmulneg1  11514  fzprval  11795  fztpval  11796  modifeq2int  12090  seqf1olem1  12190  seqf1olem2  12191  bcval2  12427  ccatval1  12649  swrdccat  12774  swrdccat3a  12775  swrdccat3b  12777  repswswrd  12812  cshword  12818  0csh0  12820  ccatco  12857  sgnn  13076  max0add  13292  absmax  13311  sumrblem  13682  fsumcvg  13683  summolem2a  13686  isum  13690  sumss  13695  sumss2  13697  fsumcvg2  13698  fsumser  13701  fsumsplit  13711  sumsplit  13734  prodrblem  13888  fprodcvg  13889  prodmolem2a  13893  zprod  13896  iprod  13897  iprodn0  13899  prodss  13906  fprodsplit  13922  ruclem2  14174  ruclem3  14175  sadadd2lem2  14309  sadcf  14312  sadc0  14313  sadcp1  14314  sadcaddlem  14316  smupf  14337  smup0  14338  gcd0val  14356  eucalgf  14421  eucalginv  14422  eucalglt  14423  pc0  14587  pcgcd  14610  pcmptcl  14619  pcmpt  14620  pcmpt2  14621  pcprod  14623  fldivp1  14625  prmreclem2  14644  prmreclem4  14646  1arithlem4  14653  vdwlem6  14713  ramtcl2  14738  ramcl2  14743  ramub1lem1  14753  ressid2  14896  xpscfv  15176  xpsfrnel  15177  xpsaddlem  15189  xpsvsca  15193  gsumval1  16228  mgm2nsgrplem2  16361  sgrp2nmndlem2  16366  symgextfve  16768  symgfixfolem1  16787  pmtrmvd  16805  pmtrfinv  16810  pmtrprfval  16836  pmtrprfvalrn  16837  frgpuptinv  17113  frgpup2  17118  frgpup3lem  17119  cyggex  17224  gsumzsplit  17268  gsumzsplitOLD  17269  gsummpt1n0  17313  dprdfid  17377  dprdfidOLD  17384  dmdprdsplitlem  17404  dmdprdsplitlemOLD  17405  abvtrivd  17809  psrlidm  18376  psrlidmOLD  18377  psrridm  18378  psrridmOLD  18379  mvrf1  18401  mplmonmul  18446  mplcoe1  18447  mplcoe3  18448  mplcoe3OLD  18449  mplcoe5  18451  mplcoe2OLD  18453  mplmon2  18478  subrgasclcl  18484  evlslem3  18503  evlslem1  18504  coe1tmfv1  18635  ply1sclid  18649  znf1o  18888  uvcvv1  19116  dmatmul  19291  scmatscmiddistr  19302  1mavmul  19342  mulmarep1gsum2  19368  1marepvmarrepid  19369  mdetdiag  19393  mdetralt2  19403  mdetunilem2  19407  mdetunilem7  19412  mdetunilem8  19413  mdetunilem9  19414  mndifsplit  19430  maducoeval2  19434  madugsum  19437  madurid  19438  gsummatr01lem3  19451  gsummatr01  19453  smadiadetglem2  19466  1elcpmat  19508  decpmatid  19563  chfacfscmulgsum  19653  chfacfpmmulgsum  19657  ptpjpre1  20364  ptbasfi  20374  ptpjopn  20405  isfcls  20802  ptcmplem2  20845  ptcmplem3  20846  tsmssplit  20946  dscmet  21385  dscopn  21386  icccmplem2  21620  iccpnfcnv  21736  xrhmeo  21738  pcohtpylem  21811  pcopt  21814  pcopt2  21815  pcoass  21816  pcorevlem  21818  cmetcaulem  22019  ovolicc1  22219  ioorcl  22278  i1f1lem  22388  itg11  22390  itg1addlem2  22396  itg1addlem4  22398  i1fres  22404  itg1climres  22413  mbfi1fseqlem4  22417  mbfi1fseqlem5  22418  mbfi1flim  22422  itg2const2  22440  itg2seq  22441  itg2uba  22442  itg2splitlem  22447  itg2split  22448  itg2monolem1  22449  itg2cnlem1  22460  itg2cnlem2  22461  iblcnlem  22487  iblss  22503  iblss2  22504  itgitg2  22505  itgle  22508  itgss  22510  itgss2  22511  itgss3  22513  itgless  22515  ibladdlem  22518  itgaddlem1  22521  iblabslem  22526  iblabs  22527  iblabsr  22528  iblmulc2  22529  bddmulibl  22537  itggt0  22540  itgcn  22541  limcvallem  22567  ellimc2  22573  limccnp  22587  limccnp2  22588  limcco  22589  dvcobr  22641  dvexp2  22649  elply2  22885  elplyd  22891  ply1termlem  22892  coe1termlem  22947  abelthlem9  23127  logtayl  23335  leibpilem2  23597  leibpi  23598  rlimcnp2  23622  efrlim  23625  igamz  23703  isnsqf  23790  mule1  23803  sqff1o  23837  muinv  23850  chtublem  23867  dchrelbasd  23895  bposlem1  23940  bposlem3  23942  bposlem5  23944  bposlem6  23945  lgsval2lem  23962  lgsneg  23975  lgsdilem  23978  lgsdir2  23984  lgsdir  23986  lgsdi  23988  lgsne0  23989  dchrvmasum2if  24063  dchrvmasumiflem1  24067  rpvmasum2  24078  pntrlog2bndlem4  24146  pntrlog2bndlem5  24147  padicabv  24196  ostth2lem4  24202  axlowdimlem15  24676  ifbieq12d2  27841  elimifd  27842  elim2if  27843  resvid2  28271  xrge0iifcnv  28368  xrge0iifiso  28370  xrge0iifhom  28372  indval2  28462  ind1  28466  sigaclfu2  28569  ddeval1  28683  eulerpartlemb  28813  ballotlemsima  28960  ballotlemrv1  28965  signsw0glem  29016  signswmnd  29020  signswrid  29021  indispcon  29531  mrsubvr  29723  dfrdg2  30015  dfrdg3  30016  unisnif  30263  dfrdg4  30289  fnejoin2  30597  bj-xpima2sn  31080  mblfinlem2  31424  mbfposadd  31434  itg2addnclem  31439  itg2gt0cn  31443  ibladdnclem  31444  itgaddnclem1  31446  iblabsnclem  31451  iblabsnc  31452  iblmulc2nc  31453  bddiblnc  31458  itggt0cn  31460  ftc1anclem4  31466  ftc1anclem5  31467  ftc1anclem6  31468  ftc1anclem7  31469  ftc1anclem8  31470  ftc1anc  31471  areacirclem5  31482  areacirc  31483  fdc  31520  heiborlem4  31592  ac6s6  31862  cdleme27a  33386  cdleme31sn1  33400  cdleme31fv1  33410  cdlemk40t  33937  dihvalb  34257  pw2f1ocnv  35341  aomclem5  35366  kelac1  35371  sdrgacs  35514  phisum  35523  mon1pid  35529  arearect  35547  areaquad  35548  refsum2cnlem1  36792  upbdrech2  36877  lptioo2  37005  lptioo1  37006  coskpi2  37034  cosknegpi  37037  cncfiooicclem1  37064  cncfiooiccre  37066  dvnxpaek  37107  dvnprodlem1  37111  dvnprodlem3  37113  itgioocnicc  37144  iblcncfioo  37145  dirkerper  37246  dirkertrigeq  37251  dirkercncflem2  37254  fourierdlem10  37267  fourierdlem32  37289  fourierdlem33  37290  fourierdlem37  37294  fourierdlem62  37319  fourierdlem73  37330  fourierdlem74  37331  fourierdlem75  37332  fourierdlem79  37336  fourierdlem81  37338  fourierdlem82  37339  fourierdlem93  37350  fourierdlem97  37354  fourierdlem101  37358  fourierdlem103  37360  fourierdlem104  37361  sqwvfoura  37379  sqwvfourb  37380  fourierswlem  37381  fouriersw  37382  etransclem4  37389  etransclem15  37400  etransclem19  37404  etransclem20  37405  etransclem23  37408  etransclem24  37409  etransclem25  37410  etransclem27  37412  etransclem31  37416  etransclem32  37417  afvfundmfveq  37591  pfxccat3a  37916  cshword2  37924  linc1  38537  lincext3  38568  lindslinindsimp1  38569  el0ldep  38578  islindeps2  38595