Theorem iftrue 3645

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 3639	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
2		dedlema 982	. . 3 |- ( ph -> ( x e. A <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
3	2	abbi2dv 2359	. 2 |- ( ph -> A = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
4	1, 3	eqtr4id 2290	1 |- ( ph -> if ( ph , A , B ) = A )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 720   = wceq 1402   e. wcel 2209   {cab 2224   ifcif 3638

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-if 3639

This theorem is used by:  iftruei  3646  iftrued  3647  ifsbdc  3653  ifcldadc  3670  ifeqdadc  3673  ifbothdadc  3674  ifbothdc  3675  ifiddc  3676  ifcldcd  3678  ifnotdc  3679  2if2dc  3680  ifandc  3681  ifordc  3682  ifnefals  3685  pw2f1odclem  7140  fidifsnen  7178  nnnninf  7472  nnnninf2  7473  mkvprop  7504  iftrueb01  7588  ind1  9309  uzin  9970  fzprval  10505  fztpval  10506  modifeq2int  10843  seqf1oglem1  10976  seqf1oglem2  10977  bcval  11208  bcval2  11209  ccatval1  11386  ccatalpha  11402  swrdccat  11528  pfxccat3a  11531  swrdccat3b  11533  sumrbdclem  12168  fsum3cvg  12169  summodclem2a  12172  isumss2  12184  fsum3ser  12188  fsumsplit  12198  sumsplitdc  12223  prodrbdclem  12362  fproddccvg  12363  iprodap  12371  iprodap0  12373  prodssdc  12380  fprodsplitdc  12387  flodddiv4  12727  gcd0val  12761  dfgcd2  12815  eucalgf  12857  eucalginv  12858  eucalglt  12859  phisum  13047  pc0  13111  pcgcd  13136  pcmptcl  13149  pcmpt  13150  pcmpt2  13151  pcprod  13153  fldivp1  13155  1arithlem4  13173  ballotfilemsima  13316  ballotfilemrv1  13321  unct  13390  xpsfrnel  13723  znf1o  15094  psrlidmfi  15208  psrridmfi  15209  mvrf1fi  15219  dvexp2  15955  elply2  15978  elplyd  15984  ply1termlem  15985  chtublem  16312  bposlem1  16328  bposlem3  16330  bposlem5  16332  bposlem6  16333  lgsval2lem  16351  lgsneg  16365  lgsdilem  16368  lgsdir2  16374  lgsdir  16376  lgsdi  16378  lgsne0  16379  gausslemma2dlem1a  16399  2lgslem1c  16431  2lgslem3  16442  2lgs  16445  opvtxval  16484  opiedgval  16487  depindlem1  16969  nnsf  17271  nninfsellemsuc  17278