Theorem iftrue 3607

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		df-if 3603	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
2		dedlema 975	. . 3 |- ( ph -> ( x e. A <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
3	2	abbi2dv 2348	. 2 |- ( ph -> A = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
4	1, 3	eqtr4id 2281	1 |- ( ph -> if ( ph , A , B ) = A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 713   = wceq 1395   e. wcel 2200   {cab 2215   ifcif 3602

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-if 3603

This theorem is referenced by:  iftruei  3608  iftrued  3609  ifsbdc  3615  ifcldadc  3632  ifeqdadc  3635  ifbothdadc  3636  ifbothdc  3637  ifiddc  3638  ifcldcd  3640  ifnotdc  3641  2if2dc  3642  ifandc  3643  ifordc  3644  ifnefals  3647  pw2f1odclem  7003  fidifsnen  7040  nnnninf  7304  nnnninf2  7305  mkvprop  7336  iftrueb01  7419  uzin  9767  fzprval  10290  fztpval  10291  modifeq2int  10620  seqf1oglem1  10753  seqf1oglem2  10754  bcval  10983  bcval2  10984  ccatval1  11145  ccatalpha  11161  swrdccat  11283  pfxccat3a  11286  swrdccat3b  11288  sumrbdclem  11904  fsum3cvg  11905  summodclem2a  11908  isumss2  11920  fsum3ser  11924  fsumsplit  11934  sumsplitdc  11959  prodrbdclem  12098  fproddccvg  12099  iprodap  12107  iprodap0  12109  prodssdc  12116  fprodsplitdc  12123  flodddiv4  12463  gcd0val  12497  dfgcd2  12551  eucalgf  12593  eucalginv  12594  eucalglt  12595  phisum  12779  pc0  12843  pcgcd  12868  pcmptcl  12881  pcmpt  12882  pcmpt2  12883  pcprod  12885  fldivp1  12887  1arithlem4  12905  unct  13029  xpsfrnel  13393  znf1o  14631  dvexp2  15402  elply2  15425  elplyd  15431  ply1termlem  15432  lgsval2lem  15705  lgsneg  15719  lgsdilem  15722  lgsdir2  15728  lgsdir  15730  lgsdi  15732  lgsne0  15733  gausslemma2dlem1a  15753  2lgslem1c  15785  2lgslem3  15796  2lgs  15799  opvtxval  15838  opiedgval  15841  nnsf  16459  nninfsellemsuc  16466