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  7138  fidifsnen  7176  nnnninf  7472  nnnninf2  7473  mkvprop  7504  iftrueb01  7588  ind1  9309  uzin  9971  fzprval  10506  fztpval  10507  modifeq2int  10844  seqf1oglem1  10977  seqf1oglem2  10978  bcval  11209  bcval2  11210  ccatval1  11387  ccatalpha  11403  swrdccat  11529  pfxccat3a  11532  swrdccat3b  11534  sumrbdclem  12169  fsum3cvg  12170  summodclem2a  12173  isumss2  12185  fsum3ser  12189  fsumsplit  12199  sumsplitdc  12224  prodrbdclem  12363  fproddccvg  12364  iprodap  12372  iprodap0  12374  prodssdc  12381  fprodsplitdc  12388  flodddiv4  12728  gcd0val  12762  dfgcd2  12816  eucalgf  12858  eucalginv  12859  eucalglt  12860  phisum  13048  pc0  13112  pcgcd  13137  pcmptcl  13150  pcmpt  13151  pcmpt2  13152  pcprod  13154  fldivp1  13156  1arithlem4  13174  ballotfilemsima  13317  ballotfilemrv1  13322  unct  13391  xpsfrnel  13724  znf1o  15095  psrlidmfi  15199  psrridmfi  15200  dvexp2  15938  elply2  15961  elplyd  15967  ply1termlem  15968  chtublem  16295  bposlem1  16311  bposlem3  16313  bposlem5  16315  bposlem6  16316  lgsval2lem  16334  lgsneg  16348  lgsdilem  16351  lgsdir2  16357  lgsdir  16359  lgsdi  16361  lgsne0  16362  gausslemma2dlem1a  16382  2lgslem1c  16414  2lgslem3  16425  2lgs  16428  opvtxval  16467  opiedgval  16470  depindlem1  16952  nnsf  17254  nninfsellemsuc  17261