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  6185  fimax2gtrilemstep  7211  2omap  7324  updjudhcoinlf  7426  omp1eomlem  7440  difinfsnlem  7445  ctssdclemn0  7456  ctssdc  7459  enumctlemm  7460  nnnninfeq  7474  nninfisollemne  7477  fodju0  7493  nninfwlpoimlemg  7521  nninfwlpoimlemginf  7522  indconst1  9312  iseqf1olemnab  10958  iseqf1olemab  10959  iseqf1olemqk  10964  iseqf1olemfvp  10967  seq3f1olemqsumkj  10968  seq3f1olemqsum  10970  seq3f1oleml  10973  seq3f1o  10974  fser0const  10992  expnnval  10999  swrdval2  11444  swrdlend  11451  swrd0g  11453  2zsupmax  12014  2zinfmin  12033  xrmaxifle  12036  xrmaxiflemab  12037  xrmaxiflemlub  12038  xrmaxiflemcom  12039  summodclem3  12171  summodclem2a  12172  isum  12176  fsum3  12178  isumss  12182  fsumcl2lem  12189  fsumadd  12197  fsummulc2  12239  cvgratz  12323  prodmodclem3  12366  prodmodclem2a  12367  fprodseq  12374  prod1dc  12377  fprodmul  12382  ef0lem  12451  gcdval  12760  nninfctlemfo  12841  pcmpt  13150  pcmpt2  13151  ballotfilemsgt1  13311  ballotfilemsel1i  13313  ballotfilemsi  13315  ennnfonelemss  13358  ennnfonelemkh  13360  ennnfonelemhf1o  13361  fvprif  13722  gzsumcl  13862  mulgnn  13987  gzsumreidx  14230  gzsumsubmcl  14231  gzsummhm  14234  znf1o  15094  dvply1  16008  lgsdir2  16374  lgsne0  16379  gausslemma2dlem1a  16399  gausslemma2dlem1f1o  16401  gausslemma2dlem2  16403  1loopgrvd2fi  16768  1hevtxdg1en  16771  eupth2lem3lem4fi  16936  bj-charfun  17055  bj-charfundc  17056  subctctexmid  17252  idjudju  17269  nninfsellemeq  17280  nninfsellemeqinf  17282  nninffeq  17286  dcapnconst  17335