Theorem iftrued 3631

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

Syntax hints:   -> wi 4   = wceq 1398   ifcif 3622

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 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-if 3623

This theorem is referenced by:  ifeq2dadc  3656  eqifdc  3661  mposnif  6149  fimax2gtrilemstep  7160  2omap  7271  updjudhcoinlf  7373  omp1eomlem  7387  difinfsnlem  7392  ctssdclemn0  7403  ctssdc  7406  enumctlemm  7407  nnnninfeq  7421  nninfisollemne  7424  fodju0  7440  nninfwlpoimlemg  7468  nninfwlpoimlemginf  7469  iseqf1olemnab  10867  iseqf1olemab  10868  iseqf1olemqk  10873  iseqf1olemfvp  10876  seq3f1olemqsumkj  10877  seq3f1olemqsum  10879  seq3f1oleml  10882  seq3f1o  10883  fser0const  10901  expnnval  10908  swrdval2  11347  swrdlend  11354  swrd0g  11356  2zsupmax  11915  2zinfmin  11932  xrmaxifle  11935  xrmaxiflemab  11936  xrmaxiflemlub  11937  xrmaxiflemcom  11938  summodclem3  12070  summodclem2a  12071  isum  12075  fsum3  12077  isumss  12081  fsumcl2lem  12088  fsumadd  12096  fsummulc2  12138  cvgratz  12222  prodmodclem3  12265  prodmodclem2a  12266  fprodseq  12273  prod1dc  12276  fprodmul  12281  ef0lem  12350  gcdval  12659  nninfctlemfo  12740  pcmpt  13045  pcmpt2  13046  ennnfonelemss  13178  ennnfonelemkh  13180  ennnfonelemhf1o  13181  fvprif  13573  gsumfzz  13725  gsumfzcl  13729  mulgnn  13860  gsumfzreidx  14071  gsumfzsubmcl  14072  gsumfzmptfidmadd  14073  gsumfzmhm  14077  znf1o  14816  dvply1  15647  lgsdir2  15923  lgsne0  15928  gausslemma2dlem1a  15948  gausslemma2dlem1f1o  15950  gausslemma2dlem2  15952  1loopgrvd2fi  16317  1hevtxdg1en  16320  eupth2lem3lem4fi  16485  bj-charfun  16594  bj-charfundc  16595  subctctexmid  16791  nninfsellemeq  16809  nninfsellemeqinf  16811  nninffeq  16815  dcapnconst  16864