Theorem iftrue 3631

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 3625	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
2		dedlema 978	. . 3 |- ( ph -> ( x e. A <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
3	2	abbi2dv 2355	. 2 |- ( ph -> A = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
4	1, 3	eqtr4id 2286	1 |- ( ph -> if ( ph , A , B ) = A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 716   = wceq 1398   e. wcel 2205   {cab 2220   ifcif 3624

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 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-if 3625

This theorem is referenced by:  iftruei  3632  iftrued  3633  ifsbdc  3639  ifcldadc  3656  ifeqdadc  3659  ifbothdadc  3660  ifbothdc  3661  ifiddc  3662  ifcldcd  3664  ifnotdc  3665  2if2dc  3666  ifandc  3667  ifordc  3668  ifnefals  3671  pw2f1odclem  7100  fidifsnen  7138  nnnninf  7430  nnnninf2  7431  mkvprop  7462  iftrueb01  7546  uzin  9905  fzprval  10438  fztpval  10439  modifeq2int  10772  seqf1oglem1  10905  seqf1oglem2  10906  bcval  11136  bcval2  11137  ccatval1  11310  ccatalpha  11326  swrdccat  11452  pfxccat3a  11455  swrdccat3b  11457  sumrbdclem  12088  fsum3cvg  12089  summodclem2a  12092  isumss2  12104  fsum3ser  12108  fsumsplit  12118  sumsplitdc  12143  prodrbdclem  12282  fproddccvg  12283  iprodap  12291  iprodap0  12293  prodssdc  12300  fprodsplitdc  12307  flodddiv4  12647  gcd0val  12681  dfgcd2  12735  eucalgf  12777  eucalginv  12778  eucalglt  12779  phisum  12963  pc0  13027  pcgcd  13052  pcmptcl  13065  pcmpt  13066  pcmpt2  13067  pcprod  13069  fldivp1  13071  1arithlem4  13089  ballotfilemsima  13203  ballotfilemrv1  13208  unct  13277  xpsfrnel  13608  znf1o  14925  dvexp2  15703  elply2  15726  elplyd  15732  ply1termlem  15733  lgsval2lem  16009  lgsneg  16023  lgsdilem  16026  lgsdir2  16032  lgsdir  16034  lgsdi  16036  lgsne0  16037  gausslemma2dlem1a  16057  2lgslem1c  16089  2lgslem3  16100  2lgs  16103  opvtxval  16142  opiedgval  16145  depindlem1  16627  nnsf  16909  nninfsellemsuc  16916