Theorem iftrue 3520

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 3516	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
2		dedlema 958	. . 3 |- ( ph -> ( x e. A <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
3	2	abbi2dv 2283	. 2 |- ( ph -> A = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
4	1, 3	eqtr4id 2216	1 |- ( ph -> if ( ph , A , B ) = A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   \/ wo 698   = wceq 1342   e. wcel 2135   {cab 2150   ifcif 3515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-11 1493  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-if 3516

This theorem is referenced by:  iftruei  3521  iftrued  3522  ifsbdc  3527  ifcldadc  3544  ifbothdadc  3546  ifbothdc  3547  ifiddc  3548  ifcldcd  3550  ifandc  3551  fidifsnen  6827  nnnninf  7081  nnnninf2  7082  mkvprop  7113  uzin  9489  fzprval  10007  fztpval  10008  modifeq2int  10311  bcval  10651  bcval2  10652  sumrbdclem  11304  fsum3cvg  11305  summodclem2a  11308  isumss2  11320  fsum3ser  11324  fsumsplit  11334  sumsplitdc  11359  prodrbdclem  11498  fproddccvg  11499  iprodap  11507  iprodap0  11509  prodssdc  11516  fprodsplitdc  11523  flodddiv4  11856  gcd0val  11878  dfgcd2  11932  eucalgf  11966  eucalginv  11967  eucalglt  11968  phisum  12149  pc0  12213  pcgcd  12237  pcmptcl  12249  pcmpt  12250  pcmpt2  12251  pcprod  12253  fldivp1  12255  unct  12312  dvexp2  13217  nnsf  13719  nninfsellemsuc  13726