Theorem iftrue 3575

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 3571	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
2		dedlema 971	. . 3 |- ( ph -> ( x e. A <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
3	2	abbi2dv 2323	. 2 |- ( ph -> A = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
4	1, 3	eqtr4id 2256	1 |- ( ph -> if ( ph , A , B ) = A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 709   = wceq 1372   e. wcel 2175   {cab 2190   ifcif 3570

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 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-if 3571

This theorem is referenced by:  iftruei  3576  iftrued  3577  ifsbdc  3582  ifcldadc  3599  ifeqdadc  3602  ifbothdadc  3603  ifbothdc  3604  ifiddc  3605  ifcldcd  3607  ifnotdc  3608  ifandc  3609  ifordc  3610  ifnefals  3613  pw2f1odclem  6913  fidifsnen  6949  nnnninf  7210  nnnninf2  7211  mkvprop  7242  uzin  9663  fzprval  10186  fztpval  10187  modifeq2int  10512  seqf1oglem1  10645  seqf1oglem2  10646  bcval  10875  bcval2  10876  ccatval1  11028  sumrbdclem  11607  fsum3cvg  11608  summodclem2a  11611  isumss2  11623  fsum3ser  11627  fsumsplit  11637  sumsplitdc  11662  prodrbdclem  11801  fproddccvg  11802  iprodap  11810  iprodap0  11812  prodssdc  11819  fprodsplitdc  11826  flodddiv4  12166  gcd0val  12200  dfgcd2  12254  eucalgf  12296  eucalginv  12297  eucalglt  12298  phisum  12482  pc0  12546  pcgcd  12571  pcmptcl  12584  pcmpt  12585  pcmpt2  12586  pcprod  12588  fldivp1  12590  1arithlem4  12608  unct  12732  xpsfrnel  13094  znf1o  14331  dvexp2  15102  elply2  15125  elplyd  15131  ply1termlem  15132  lgsval2lem  15405  lgsneg  15419  lgsdilem  15422  lgsdir2  15428  lgsdir  15430  lgsdi  15432  lgsne0  15433  gausslemma2dlem1a  15453  2lgslem1c  15485  2lgslem3  15496  2lgs  15499  nnsf  15806  nninfsellemsuc  15813