Theorem iftrue 3539

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 3535	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
2		dedlema 969	. . 3 |- ( ph -> ( x e. A <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
3	2	abbi2dv 2296	. 2 |- ( ph -> A = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
4	1, 3	eqtr4id 2229	1 |- ( ph -> if ( ph , A , B ) = A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 708   = wceq 1353   e. wcel 2148   {cab 2163   ifcif 3534

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 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-if 3535

This theorem is referenced by:  iftruei  3540  iftrued  3541  ifsbdc  3546  ifcldadc  3563  ifbothdadc  3566  ifbothdc  3567  ifiddc  3568  ifcldcd  3570  ifnotdc  3571  ifandc  3572  ifordc  3573  fidifsnen  6867  nnnninf  7121  nnnninf2  7122  mkvprop  7153  uzin  9556  fzprval  10077  fztpval  10078  modifeq2int  10381  bcval  10722  bcval2  10723  sumrbdclem  11378  fsum3cvg  11379  summodclem2a  11382  isumss2  11394  fsum3ser  11398  fsumsplit  11408  sumsplitdc  11433  prodrbdclem  11572  fproddccvg  11573  iprodap  11581  iprodap0  11583  prodssdc  11590  fprodsplitdc  11597  flodddiv4  11931  gcd0val  11953  dfgcd2  12007  eucalgf  12047  eucalginv  12048  eucalglt  12049  phisum  12232  pc0  12296  pcgcd  12320  pcmptcl  12332  pcmpt  12333  pcmpt2  12334  pcprod  12336  fldivp1  12338  1arithlem4  12356  unct  12435  dvexp2  14047  lgsval2lem  14282  lgsneg  14296  lgsdilem  14299  lgsdir2  14305  lgsdir  14307  lgsdi  14309  lgsne0  14310  nnsf  14614  nninfsellemsuc  14621