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  7466  nnnninf2  7467  mkvprop  7498  iftrueb01  7582  ind1  9302  uzin  9964  fzprval  10499  fztpval  10500  modifeq2int  10836  seqf1oglem1  10969  seqf1oglem2  10970  bcval  11201  bcval2  11202  ccatval1  11379  ccatalpha  11395  swrdccat  11521  pfxccat3a  11524  swrdccat3b  11526  sumrbdclem  12160  fsum3cvg  12161  summodclem2a  12164  isumss2  12176  fsum3ser  12180  fsumsplit  12190  sumsplitdc  12215  prodrbdclem  12354  fproddccvg  12355  iprodap  12363  iprodap0  12365  prodssdc  12372  fprodsplitdc  12379  flodddiv4  12719  gcd0val  12753  dfgcd2  12807  eucalgf  12849  eucalginv  12850  eucalglt  12851  phisum  13039  pc0  13103  pcgcd  13128  pcmptcl  13141  pcmpt  13142  pcmpt2  13143  pcprod  13145  fldivp1  13147  1arithlem4  13165  ballotfilemsima  13308  ballotfilemrv1  13313  unct  13382  xpsfrnel  13714  znf1o  15035  dvexp2  15862  elply2  15885  elplyd  15891  ply1termlem  15892  bposlem1  16209  bposlem3  16211  bposlem5  16213  lgsval2lem  16227  lgsneg  16241  lgsdilem  16244  lgsdir2  16250  lgsdir  16252  lgsdi  16254  lgsne0  16255  gausslemma2dlem1a  16275  2lgslem1c  16307  2lgslem3  16318  2lgs  16321  opvtxval  16360  opiedgval  16363  depindlem1  16845  nnsf  17146  nninfsellemsuc  17153