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  11630  fsum3cvg  11631  summodclem2a  11634  isumss2  11646  fsum3ser  11650  fsumsplit  11660  sumsplitdc  11685  prodrbdclem  11824  fproddccvg  11825  iprodap  11833  iprodap0  11835  prodssdc  11842  fprodsplitdc  11849  flodddiv4  12189  gcd0val  12223  dfgcd2  12277  eucalgf  12319  eucalginv  12320  eucalglt  12321  phisum  12505  pc0  12569  pcgcd  12594  pcmptcl  12607  pcmpt  12608  pcmpt2  12609  pcprod  12611  fldivp1  12613  1arithlem4  12631  unct  12755  xpsfrnel  13118  znf1o  14355  dvexp2  15126  elply2  15149  elplyd  15155  ply1termlem  15156  lgsval2lem  15429  lgsneg  15443  lgsdilem  15446  lgsdir2  15452  lgsdir  15454  lgsdi  15456  lgsne0  15457  gausslemma2dlem1a  15477  2lgslem1c  15509  2lgslem3  15520  2lgs  15523  opvtxval  15560  opiedgval  15563  nnsf  15875  nninfsellemsuc  15882