Theorem iftrued 3577

Description: Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

Ref	Expression
iftrued.1	|- ( ph -> ch )

Assertion

Ref	Expression
iftrued	|- ( ph -> if ( ch , A , B ) = A )

Proof of Theorem iftrued

Step	Hyp	Ref	Expression
1		iftrued.1	. 2 |- ( ph -> ch )
2		iftrue 3575	. 2 |- ( ch -> if ( ch , A , B ) = A )
3	1, 2	syl 14	1 |- ( ph -> if ( ch , A , B ) = A )

Syntax hints:   -> wi 4   = wceq 1372   ifcif 3570

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 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-if 3571

This theorem is referenced by:  ifeq2dadc  3601  eqifdc  3606  mposnif  6038  fimax2gtrilemstep  6996  updjudhcoinlf  7181  omp1eomlem  7195  difinfsnlem  7200  ctssdclemn0  7211  ctssdc  7214  enumctlemm  7215  nnnninfeq  7229  nninfisollemne  7232  fodju0  7248  nninfwlpoimlemg  7276  nninfwlpoimlemginf  7277  iseqf1olemnab  10644  iseqf1olemab  10645  iseqf1olemqk  10650  iseqf1olemfvp  10653  seq3f1olemqsumkj  10654  seq3f1olemqsum  10656  seq3f1oleml  10659  seq3f1o  10660  fser0const  10678  expnnval  10685  2zsupmax  11508  2zinfmin  11525  xrmaxifle  11528  xrmaxiflemab  11529  xrmaxiflemlub  11530  xrmaxiflemcom  11531  summodclem3  11662  summodclem2a  11663  isum  11667  fsum3  11669  isumss  11673  fsumcl2lem  11680  fsumadd  11688  fsummulc2  11730  cvgratz  11814  prodmodclem3  11857  prodmodclem2a  11858  fprodseq  11865  prod1dc  11868  fprodmul  11873  ef0lem  11942  gcdval  12251  nninfctlemfo  12332  pcmpt  12637  pcmpt2  12638  ennnfonelemss  12752  ennnfonelemkh  12754  ennnfonelemhf1o  12755  fvprif  13146  gsumfzz  13298  gsumfzcl  13302  mulgnn  13433  gsumfzreidx  13644  gsumfzsubmcl  13645  gsumfzmptfidmadd  13646  gsumfzmhm  13650  znf1o  14384  dvply1  15208  lgsdir2  15481  lgsne0  15486  gausslemma2dlem1a  15506  gausslemma2dlem1f1o  15508  gausslemma2dlem2  15510  bj-charfun  15705  bj-charfundc  15706  2omap  15894  subctctexmid  15899  nninfsellemeq  15913  nninfsellemeqinf  15915  nninffeq  15919  dcapnconst  15962