Theorem iftrue 3607

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 3603	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
2		dedlema 975	. . 3 |- ( ph -> ( x e. A <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
3	2	abbi2dv 2348	. 2 |- ( ph -> A = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
4	1, 3	eqtr4id 2281	1 |- ( ph -> if ( ph , A , B ) = A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 713   = wceq 1395   e. wcel 2200   {cab 2215   ifcif 3602

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 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-if 3603

This theorem is referenced by:  iftruei  3608  iftrued  3609  ifsbdc  3615  ifcldadc  3632  ifeqdadc  3635  ifbothdadc  3636  ifbothdc  3637  ifiddc  3638  ifcldcd  3640  ifnotdc  3641  2if2dc  3642  ifandc  3643  ifordc  3644  ifnefals  3647  pw2f1odclem  6991  fidifsnen  7028  nnnninf  7289  nnnninf2  7290  mkvprop  7321  iftrueb01  7404  uzin  9751  fzprval  10274  fztpval  10275  modifeq2int  10603  seqf1oglem1  10736  seqf1oglem2  10737  bcval  10966  bcval2  10967  ccatval1  11127  swrdccat  11262  pfxccat3a  11265  swrdccat3b  11267  sumrbdclem  11883  fsum3cvg  11884  summodclem2a  11887  isumss2  11899  fsum3ser  11903  fsumsplit  11913  sumsplitdc  11938  prodrbdclem  12077  fproddccvg  12078  iprodap  12086  iprodap0  12088  prodssdc  12095  fprodsplitdc  12102  flodddiv4  12442  gcd0val  12476  dfgcd2  12530  eucalgf  12572  eucalginv  12573  eucalglt  12574  phisum  12758  pc0  12822  pcgcd  12847  pcmptcl  12860  pcmpt  12861  pcmpt2  12862  pcprod  12864  fldivp1  12866  1arithlem4  12884  unct  13008  xpsfrnel  13372  znf1o  14609  dvexp2  15380  elply2  15403  elplyd  15409  ply1termlem  15410  lgsval2lem  15683  lgsneg  15697  lgsdilem  15700  lgsdir2  15706  lgsdir  15708  lgsdi  15710  lgsne0  15711  gausslemma2dlem1a  15731  2lgslem1c  15763  2lgslem3  15774  2lgs  15777  opvtxval  15816  opiedgval  15819  nnsf  16330  nninfsellemsuc  16337