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  7134  fidifsnen  7172  nnnninf  7467  nnnninf2  7468  mkvprop  7499  iftrueb01  7583  ind1  9303  uzin  9965  fzprval  10500  fztpval  10501  modifeq2int  10838  seqf1oglem1  10971  seqf1oglem2  10972  bcval  11203  bcval2  11204  ccatval1  11381  ccatalpha  11397  swrdccat  11523  pfxccat3a  11526  swrdccat3b  11528  sumrbdclem  12163  fsum3cvg  12164  summodclem2a  12167  isumss2  12179  fsum3ser  12183  fsumsplit  12193  sumsplitdc  12218  prodrbdclem  12357  fproddccvg  12358  iprodap  12366  iprodap0  12368  prodssdc  12375  fprodsplitdc  12382  flodddiv4  12722  gcd0val  12756  dfgcd2  12810  eucalgf  12852  eucalginv  12853  eucalglt  12854  phisum  13042  pc0  13106  pcgcd  13131  pcmptcl  13144  pcmpt  13145  pcmpt2  13146  pcprod  13148  fldivp1  13150  1arithlem4  13168  ballotfilemsima  13311  ballotfilemrv1  13316  unct  13385  xpsfrnel  13718  znf1o  15070  dvexp2  15904  elply2  15927  elplyd  15933  ply1termlem  15934  chtublem  16256  bposlem1  16272  bposlem3  16274  bposlem5  16276  bposlem6  16277  lgsval2lem  16295  lgsneg  16309  lgsdilem  16312  lgsdir2  16318  lgsdir  16320  lgsdi  16322  lgsne0  16323  gausslemma2dlem1a  16343  2lgslem1c  16375  2lgslem3  16386  2lgs  16389  opvtxval  16428  opiedgval  16431  depindlem1  16913  nnsf  17214  nninfsellemsuc  17221