Theorem iftrue 3608

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 3604	. 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 3603

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 3604

This theorem is referenced by:  iftruei  3609  iftrued  3610  ifsbdc  3616  ifcldadc  3633  ifeqdadc  3636  ifbothdadc  3637  ifbothdc  3638  ifiddc  3639  ifcldcd  3641  ifnotdc  3642  2if2dc  3643  ifandc  3644  ifordc  3645  ifnefals  3648  pw2f1odclem  7015  fidifsnen  7052  nnnninf  7316  nnnninf2  7317  mkvprop  7348  iftrueb01  7431  uzin  9779  fzprval  10307  fztpval  10308  modifeq2int  10638  seqf1oglem1  10771  seqf1oglem2  10772  bcval  11001  bcval2  11002  ccatval1  11164  ccatalpha  11180  swrdccat  11306  pfxccat3a  11309  swrdccat3b  11311  sumrbdclem  11928  fsum3cvg  11929  summodclem2a  11932  isumss2  11944  fsum3ser  11948  fsumsplit  11958  sumsplitdc  11983  prodrbdclem  12122  fproddccvg  12123  iprodap  12131  iprodap0  12133  prodssdc  12140  fprodsplitdc  12147  flodddiv4  12487  gcd0val  12521  dfgcd2  12575  eucalgf  12617  eucalginv  12618  eucalglt  12619  phisum  12803  pc0  12867  pcgcd  12892  pcmptcl  12905  pcmpt  12906  pcmpt2  12907  pcprod  12909  fldivp1  12911  1arithlem4  12929  unct  13053  xpsfrnel  13417  znf1o  14655  dvexp2  15426  elply2  15449  elplyd  15455  ply1termlem  15456  lgsval2lem  15729  lgsneg  15743  lgsdilem  15746  lgsdir2  15752  lgsdir  15754  lgsdi  15756  lgsne0  15757  gausslemma2dlem1a  15777  2lgslem1c  15809  2lgslem3  15820  2lgs  15823  opvtxval  15862  opiedgval  15865  nnsf  16543  nninfsellemsuc  16550