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  9303  iseqf1olemnab  10938  iseqf1olemab  10939  iseqf1olemqk  10944  iseqf1olemfvp  10947  seq3f1olemqsumkj  10948  seq3f1olemqsum  10950  seq3f1oleml  10953  seq3f1o  10954  fser0const  10972  expnnval  10979  swrdval2  11423  swrdlend  11430  swrd0g  11432  2zsupmax  11992  2zinfmin  12009  xrmaxifle  12012  xrmaxiflemab  12013  xrmaxiflemlub  12014  xrmaxiflemcom  12015  summodclem3  12147  summodclem2a  12148  isum  12152  fsum3  12154  isumss  12158  fsumcl2lem  12165  fsumadd  12173  fsummulc2  12215  cvgratz  12299  prodmodclem3  12342  prodmodclem2a  12343  fprodseq  12350  prod1dc  12353  fprodmul  12358  ef0lem  12427  gcdval  12736  nninfctlemfo  12817  pcmpt  13122  pcmpt2  13123  ballotfilemsgt1  13254  ballotfilemsel1i  13256  ballotfilemsi  13258  ennnfonelemss  13301  ennnfonelemkh  13303  ennnfonelemhf1o  13304  fvprif  13664  gzsumcl  13804  mulgnn  13929  gzsumreidx  14141  gzsumsubmcl  14142  gzsummhm  14145  znf1o  14986  dvply1  15866  lgsdir2  16152  lgsne0  16157  gausslemma2dlem1a  16177  gausslemma2dlem1f1o  16179  gausslemma2dlem2  16181  1loopgrvd2fi  16546  1hevtxdg1en  16549  eupth2lem3lem4fi  16714  bj-charfun  16833  bj-charfundc  16834  subctctexmid  17030  nninfsellemeq  17057  nninfsellemeqinf  17059  nninffeq  17063  dcapnconst  17111