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  9300  uzin  9955  fzprval  10489  fztpval  10490  modifeq2int  10823  seqf1oglem1  10956  seqf1oglem2  10957  bcval  11187  bcval2  11188  ccatval1  11365  ccatalpha  11381  swrdccat  11507  pfxccat3a  11510  swrdccat3b  11512  sumrbdclem  12144  fsum3cvg  12145  summodclem2a  12148  isumss2  12160  fsum3ser  12164  fsumsplit  12174  sumsplitdc  12199  prodrbdclem  12338  fproddccvg  12339  iprodap  12347  iprodap0  12349  prodssdc  12356  fprodsplitdc  12363  flodddiv4  12703  gcd0val  12737  dfgcd2  12791  eucalgf  12833  eucalginv  12834  eucalglt  12835  phisum  13019  pc0  13083  pcgcd  13108  pcmptcl  13121  pcmpt  13122  pcmpt2  13123  pcprod  13125  fldivp1  13127  1arithlem4  13145  ballotfilemsima  13259  ballotfilemrv1  13264  unct  13333  xpsfrnel  13665  znf1o  14986  dvexp2  15813  elply2  15836  elplyd  15842  ply1termlem  15843  lgsval2lem  16129  lgsneg  16143  lgsdilem  16146  lgsdir2  16152  lgsdir  16154  lgsdi  16156  lgsne0  16157  gausslemma2dlem1a  16177  2lgslem1c  16209  2lgslem3  16220  2lgs  16223  opvtxval  16262  opiedgval  16265  depindlem1  16747  nnsf  17048  nninfsellemsuc  17055