Theorem iftrue 3627

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 3621	. 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 2353	. 2 |- ( ph -> A = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
4	1, 3	eqtr4id 2284	1 |- ( ph -> if ( ph , A , B ) = A )

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

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-if 3621

This theorem is referenced by:  iftruei  3628  iftrued  3629  ifsbdc  3635  ifcldadc  3652  ifeqdadc  3655  ifbothdadc  3656  ifbothdc  3657  ifiddc  3658  ifcldcd  3660  ifnotdc  3661  2if2dc  3662  ifandc  3663  ifordc  3664  ifnefals  3667  pw2f1odclem  7087  fidifsnen  7125  nnnninf  7417  nnnninf2  7418  mkvprop  7449  iftrueb01  7533  uzin  9887  fzprval  10416  fztpval  10417  modifeq2int  10748  seqf1oglem1  10881  seqf1oglem2  10882  bcval  11111  bcval2  11112  ccatval1  11285  ccatalpha  11301  swrdccat  11427  pfxccat3a  11430  swrdccat3b  11432  sumrbdclem  12063  fsum3cvg  12064  summodclem2a  12067  isumss2  12079  fsum3ser  12083  fsumsplit  12093  sumsplitdc  12118  prodrbdclem  12257  fproddccvg  12258  iprodap  12266  iprodap0  12268  prodssdc  12275  fprodsplitdc  12282  flodddiv4  12622  gcd0val  12656  dfgcd2  12710  eucalgf  12752  eucalginv  12753  eucalglt  12754  phisum  12938  pc0  13002  pcgcd  13027  pcmptcl  13040  pcmpt  13041  pcmpt2  13042  pcprod  13044  fldivp1  13046  1arithlem4  13064  unct  13193  xpsfrnel  13557  znf1o  14799  dvexp2  15577  elply2  15600  elplyd  15606  ply1termlem  15607  lgsval2lem  15883  lgsneg  15897  lgsdilem  15900  lgsdir2  15906  lgsdir  15908  lgsdi  15910  lgsne0  15911  gausslemma2dlem1a  15931  2lgslem1c  15963  2lgslem3  15974  2lgs  15977  opvtxval  16016  opiedgval  16019  depindlem1  16501  nnsf  16783  nninfsellemsuc  16790