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  7319  updjudhcoinlf  7421  omp1eomlem  7435  difinfsnlem  7440  ctssdclemn0  7451  ctssdc  7454  enumctlemm  7455  nnnninfeq  7469  nninfisollemne  7472  fodju0  7488  nninfwlpoimlemg  7516  nninfwlpoimlemginf  7517  indconst1  9306  iseqf1olemnab  10953  iseqf1olemab  10954  iseqf1olemqk  10959  iseqf1olemfvp  10962  seq3f1olemqsumkj  10963  seq3f1olemqsum  10965  seq3f1oleml  10968  seq3f1o  10969  fser0const  10987  expnnval  10994  swrdval2  11439  swrdlend  11446  swrd0g  11448  2zsupmax  12009  2zinfmin  12028  xrmaxifle  12031  xrmaxiflemab  12032  xrmaxiflemlub  12033  xrmaxiflemcom  12034  summodclem3  12166  summodclem2a  12167  isum  12171  fsum3  12173  isumss  12177  fsumcl2lem  12184  fsumadd  12192  fsummulc2  12234  cvgratz  12318  prodmodclem3  12361  prodmodclem2a  12362  fprodseq  12369  prod1dc  12372  fprodmul  12377  ef0lem  12446  gcdval  12755  nninfctlemfo  12836  pcmpt  13145  pcmpt2  13146  ballotfilemsgt1  13306  ballotfilemsel1i  13308  ballotfilemsi  13310  ennnfonelemss  13353  ennnfonelemkh  13355  ennnfonelemhf1o  13356  fvprif  13717  gzsumcl  13857  mulgnn  13982  gzsumreidx  14225  gzsumsubmcl  14226  gzsummhm  14229  znf1o  15070  dvply1  15957  lgsdir2  16318  lgsne0  16323  gausslemma2dlem1a  16343  gausslemma2dlem1f1o  16345  gausslemma2dlem2  16347  1loopgrvd2fi  16712  1hevtxdg1en  16715  eupth2lem3lem4fi  16880  bj-charfun  16999  bj-charfundc  17000  subctctexmid  17196  nninfsellemeq  17223  nninfsellemeqinf  17225  nninffeq  17229  dcapnconst  17278