Theorem iftrued 3610

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

Syntax hints:   -> wi 4   = wceq 1395   ifcif 3603

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 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-if 3604

This theorem is referenced by:  ifeq2dadc  3635  eqifdc  3640  mposnif  6110  fimax2gtrilemstep  7083  updjudhcoinlf  7270  omp1eomlem  7284  difinfsnlem  7289  ctssdclemn0  7300  ctssdc  7303  enumctlemm  7304  nnnninfeq  7318  nninfisollemne  7321  fodju0  7337  nninfwlpoimlemg  7365  nninfwlpoimlemginf  7366  iseqf1olemnab  10753  iseqf1olemab  10754  iseqf1olemqk  10759  iseqf1olemfvp  10762  seq3f1olemqsumkj  10763  seq3f1olemqsum  10765  seq3f1oleml  10768  seq3f1o  10769  fser0const  10787  expnnval  10794  swrdval2  11222  swrdlend  11229  swrd0g  11231  2zsupmax  11777  2zinfmin  11794  xrmaxifle  11797  xrmaxiflemab  11798  xrmaxiflemlub  11799  xrmaxiflemcom  11800  summodclem3  11931  summodclem2a  11932  isum  11936  fsum3  11938  isumss  11942  fsumcl2lem  11949  fsumadd  11957  fsummulc2  11999  cvgratz  12083  prodmodclem3  12126  prodmodclem2a  12127  fprodseq  12134  prod1dc  12137  fprodmul  12142  ef0lem  12211  gcdval  12520  nninfctlemfo  12601  pcmpt  12906  pcmpt2  12907  ennnfonelemss  13021  ennnfonelemkh  13023  ennnfonelemhf1o  13024  fvprif  13416  gsumfzz  13568  gsumfzcl  13572  mulgnn  13703  gsumfzreidx  13914  gsumfzsubmcl  13915  gsumfzmptfidmadd  13916  gsumfzmhm  13920  znf1o  14655  dvply1  15479  lgsdir2  15752  lgsne0  15757  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  gausslemma2dlem2  15781  1loopgrvd2fi  16111  bj-charfun  16338  bj-charfundc  16339  2omap  16530  subctctexmid  16537  nninfsellemeq  16552  nninfsellemeqinf  16554  nninffeq  16558  dcapnconst  16601