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 )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   ifcif 3638

This proof depends on 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 proof 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 used by:  ifeq2dadc  3672  eqifdc  3677  ifeqeqxdc  3687  mposnif  6182  fimax2gtrilemstep  7205  2omap  7318  updjudhcoinlf  7420  omp1eomlem  7434  difinfsnlem  7439  ctssdclemn0  7450  ctssdc  7453  enumctlemm  7454  nnnninfeq  7468  nninfisollemne  7471  fodju0  7487  nninfwlpoimlemg  7515  nninfwlpoimlemginf  7516  indconst1  9305  iseqf1olemnab  10951  iseqf1olemab  10952  iseqf1olemqk  10957  iseqf1olemfvp  10960  seq3f1olemqsumkj  10961  seq3f1olemqsum  10963  seq3f1oleml  10966  seq3f1o  10967  fser0const  10985  expnnval  10992  swrdval2  11437  swrdlend  11444  swrd0g  11446  2zsupmax  12007  2zinfmin  12025  xrmaxifle  12028  xrmaxiflemab  12029  xrmaxiflemlub  12030  xrmaxiflemcom  12031  summodclem3  12163  summodclem2a  12164  isum  12168  fsum3  12170  isumss  12174  fsumcl2lem  12181  fsumadd  12189  fsummulc2  12231  cvgratz  12315  prodmodclem3  12358  prodmodclem2a  12359  fprodseq  12366  prod1dc  12369  fprodmul  12374  ef0lem  12443  gcdval  12752  nninfctlemfo  12833  pcmpt  13142  pcmpt2  13143  ballotfilemsgt1  13303  ballotfilemsel1i  13305  ballotfilemsi  13307  ennnfonelemss  13350  ennnfonelemkh  13352  ennnfonelemhf1o  13353  fvprif  13713  gzsumcl  13853  mulgnn  13978  gzsumreidx  14190  gzsumsubmcl  14191  gzsummhm  14194  znf1o  15035  dvply1  15915  lgsdir2  16250  lgsne0  16255  gausslemma2dlem1a  16275  gausslemma2dlem1f1o  16277  gausslemma2dlem2  16279  1loopgrvd2fi  16644  1hevtxdg1en  16647  eupth2lem3lem4fi  16812  bj-charfun  16931  bj-charfundc  16932  subctctexmid  17128  nninfsellemeq  17155  nninfsellemeqinf  17157  nninffeq  17161  dcapnconst  17209