Theorem iftrued 3578

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 3576	. 2 |- ( ch -> if ( ch , A , B ) = A )
3	1, 2	syl 14	1 |- ( ph -> if ( ch , A , B ) = A )

Syntax hints:   -> wi 4   = wceq 1373   ifcif 3571

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-if 3572

This theorem is referenced by:  ifeq2dadc  3602  eqifdc  3607  mposnif  6039  fimax2gtrilemstep  6997  updjudhcoinlf  7182  omp1eomlem  7196  difinfsnlem  7201  ctssdclemn0  7212  ctssdc  7215  enumctlemm  7216  nnnninfeq  7230  nninfisollemne  7233  fodju0  7249  nninfwlpoimlemg  7277  nninfwlpoimlemginf  7278  iseqf1olemnab  10646  iseqf1olemab  10647  iseqf1olemqk  10652  iseqf1olemfvp  10655  seq3f1olemqsumkj  10656  seq3f1olemqsum  10658  seq3f1oleml  10661  seq3f1o  10662  fser0const  10680  expnnval  10687  swrdval2  11104  swrdlend  11111  swrd0g  11113  2zsupmax  11537  2zinfmin  11554  xrmaxifle  11557  xrmaxiflemab  11558  xrmaxiflemlub  11559  xrmaxiflemcom  11560  summodclem3  11691  summodclem2a  11692  isum  11696  fsum3  11698  isumss  11702  fsumcl2lem  11709  fsumadd  11717  fsummulc2  11759  cvgratz  11843  prodmodclem3  11886  prodmodclem2a  11887  fprodseq  11894  prod1dc  11897  fprodmul  11902  ef0lem  11971  gcdval  12280  nninfctlemfo  12361  pcmpt  12666  pcmpt2  12667  ennnfonelemss  12781  ennnfonelemkh  12783  ennnfonelemhf1o  12784  fvprif  13175  gsumfzz  13327  gsumfzcl  13331  mulgnn  13462  gsumfzreidx  13673  gsumfzsubmcl  13674  gsumfzmptfidmadd  13675  gsumfzmhm  13679  znf1o  14413  dvply1  15237  lgsdir2  15510  lgsne0  15515  gausslemma2dlem1a  15535  gausslemma2dlem1f1o  15537  gausslemma2dlem2  15539  bj-charfun  15743  bj-charfundc  15744  2omap  15932  subctctexmid  15937  nninfsellemeq  15951  nninfsellemeqinf  15953  nninffeq  15957  dcapnconst  16000