Theorem iftrued 3647

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

Syntax hints:   -> wi 4   = wceq 1402   ifcif 3638

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 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-if 3639

This theorem is referenced by:  ifeq2dadc  3672  eqifdc  3677  ifeqeqxdc  3687  mposnif  6175  fimax2gtrilemstep  7198  2omap  7311  updjudhcoinlf  7413  omp1eomlem  7427  difinfsnlem  7432  ctssdclemn0  7443  ctssdc  7446  enumctlemm  7447  nnnninfeq  7461  nninfisollemne  7464  fodju0  7480  nninfwlpoimlemg  7508  nninfwlpoimlemginf  7509  iseqf1olemnab  10919  iseqf1olemab  10920  iseqf1olemqk  10925  iseqf1olemfvp  10928  seq3f1olemqsumkj  10929  seq3f1olemqsum  10931  seq3f1oleml  10934  seq3f1o  10935  fser0const  10953  expnnval  10960  swrdval2  11404  swrdlend  11411  swrd0g  11413  2zsupmax  11973  2zinfmin  11990  xrmaxifle  11993  xrmaxiflemab  11994  xrmaxiflemlub  11995  xrmaxiflemcom  11996  summodclem3  12128  summodclem2a  12129  isum  12133  fsum3  12135  isumss  12139  fsumcl2lem  12146  fsumadd  12154  fsummulc2  12196  cvgratz  12280  prodmodclem3  12323  prodmodclem2a  12324  fprodseq  12331  prod1dc  12334  fprodmul  12339  ef0lem  12408  gcdval  12717  nninfctlemfo  12798  pcmpt  13103  pcmpt2  13104  ballotfilemsgt1  13235  ballotfilemsel1i  13237  ballotfilemsi  13239  ennnfonelemss  13282  ennnfonelemkh  13284  ennnfonelemhf1o  13285  fvprif  13644  gzsumcl  13784  mulgnn  13909  gzsumreidx  14121  gzsumsubmcl  14122  gzsummhm  14125  znf1o  14961  dvply1  15792  lgsdir2  16069  lgsne0  16074  gausslemma2dlem1a  16094  gausslemma2dlem1f1o  16096  gausslemma2dlem2  16098  1loopgrvd2fi  16463  1hevtxdg1en  16466  eupth2lem3lem4fi  16631  bj-charfun  16750  bj-charfundc  16751  subctctexmid  16947  nninfsellemeq  16965  nninfsellemeqinf  16967  nninffeq  16971  dcapnconst  17019