Theorem iftrue 3575

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 3571	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
2		dedlema 971	. . 3 |- ( ph -> ( x e. A <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
3	2	abbi2dv 2323	. 2 |- ( ph -> A = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
4	1, 3	eqtr4id 2256	1 |- ( ph -> if ( ph , A , B ) = A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 709   = wceq 1372   e. wcel 2175   {cab 2190   ifcif 3570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-if 3571

This theorem is referenced by:  iftruei  3576  iftrued  3577  ifsbdc  3582  ifcldadc  3599  ifeqdadc  3602  ifbothdadc  3603  ifbothdc  3604  ifiddc  3605  ifcldcd  3607  ifnotdc  3608  ifandc  3609  ifordc  3610  ifnefals  3613  pw2f1odclem  6930  fidifsnen  6966  nnnninf  7227  nnnninf2  7228  mkvprop  7259  uzin  9680  fzprval  10203  fztpval  10204  modifeq2int  10529  seqf1oglem1  10662  seqf1oglem2  10663  bcval  10892  bcval2  10893  ccatval1  11051  sumrbdclem  11659  fsum3cvg  11660  summodclem2a  11663  isumss2  11675  fsum3ser  11679  fsumsplit  11689  sumsplitdc  11714  prodrbdclem  11853  fproddccvg  11854  iprodap  11862  iprodap0  11864  prodssdc  11871  fprodsplitdc  11878  flodddiv4  12218  gcd0val  12252  dfgcd2  12306  eucalgf  12348  eucalginv  12349  eucalglt  12350  phisum  12534  pc0  12598  pcgcd  12623  pcmptcl  12636  pcmpt  12637  pcmpt2  12638  pcprod  12640  fldivp1  12642  1arithlem4  12660  unct  12784  xpsfrnel  13147  znf1o  14384  dvexp2  15155  elply2  15178  elplyd  15184  ply1termlem  15185  lgsval2lem  15458  lgsneg  15472  lgsdilem  15475  lgsdir2  15481  lgsdir  15483  lgsdi  15485  lgsne0  15486  gausslemma2dlem1a  15506  2lgslem1c  15538  2lgslem3  15549  2lgs  15552  opvtxval  15589  opiedgval  15592  nnsf  15904  nninfsellemsuc  15911