Theorem iftrue 3614

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

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

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-if 3608

This theorem is referenced by:  iftruei  3615  iftrued  3616  ifsbdc  3622  ifcldadc  3639  ifeqdadc  3642  ifbothdadc  3643  ifbothdc  3644  ifiddc  3645  ifcldcd  3647  ifnotdc  3648  2if2dc  3649  ifandc  3650  ifordc  3651  ifnefals  3654  pw2f1odclem  7063  fidifsnen  7100  nnnninf  7368  nnnninf2  7369  mkvprop  7400  iftrueb01  7484  uzin  9833  fzprval  10362  fztpval  10363  modifeq2int  10694  seqf1oglem1  10827  seqf1oglem2  10828  bcval  11057  bcval2  11058  ccatval1  11223  ccatalpha  11239  swrdccat  11365  pfxccat3a  11368  swrdccat3b  11370  sumrbdclem  12001  fsum3cvg  12002  summodclem2a  12005  isumss2  12017  fsum3ser  12021  fsumsplit  12031  sumsplitdc  12056  prodrbdclem  12195  fproddccvg  12196  iprodap  12204  iprodap0  12206  prodssdc  12213  fprodsplitdc  12220  flodddiv4  12560  gcd0val  12594  dfgcd2  12648  eucalgf  12690  eucalginv  12691  eucalglt  12692  phisum  12876  pc0  12940  pcgcd  12965  pcmptcl  12978  pcmpt  12979  pcmpt2  12980  pcprod  12982  fldivp1  12984  1arithlem4  13002  unct  13126  xpsfrnel  13490  znf1o  14730  dvexp2  15506  elply2  15529  elplyd  15535  ply1termlem  15536  lgsval2lem  15812  lgsneg  15826  lgsdilem  15829  lgsdir2  15835  lgsdir  15837  lgsdi  15839  lgsne0  15840  gausslemma2dlem1a  15860  2lgslem1c  15892  2lgslem3  15903  2lgs  15906  opvtxval  15945  opiedgval  15948  depindlem1  16430  nnsf  16714  nninfsellemsuc  16721