Theorem iftrued 3612

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

Syntax hints:   -> wi 4   = wceq 1397   ifcif 3605

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-if 3606

This theorem is referenced by:  ifeq2dadc  3637  eqifdc  3642  mposnif  6115  fimax2gtrilemstep  7090  updjudhcoinlf  7279  omp1eomlem  7293  difinfsnlem  7298  ctssdclemn0  7309  ctssdc  7312  enumctlemm  7313  nnnninfeq  7327  nninfisollemne  7330  fodju0  7346  nninfwlpoimlemg  7374  nninfwlpoimlemginf  7375  iseqf1olemnab  10763  iseqf1olemab  10764  iseqf1olemqk  10769  iseqf1olemfvp  10772  seq3f1olemqsumkj  10773  seq3f1olemqsum  10775  seq3f1oleml  10778  seq3f1o  10779  fser0const  10797  expnnval  10804  swrdval2  11232  swrdlend  11239  swrd0g  11241  2zsupmax  11787  2zinfmin  11804  xrmaxifle  11807  xrmaxiflemab  11808  xrmaxiflemlub  11809  xrmaxiflemcom  11810  summodclem3  11942  summodclem2a  11943  isum  11947  fsum3  11949  isumss  11953  fsumcl2lem  11960  fsumadd  11968  fsummulc2  12010  cvgratz  12094  prodmodclem3  12137  prodmodclem2a  12138  fprodseq  12145  prod1dc  12148  fprodmul  12153  ef0lem  12222  gcdval  12531  nninfctlemfo  12612  pcmpt  12917  pcmpt2  12918  ennnfonelemss  13032  ennnfonelemkh  13034  ennnfonelemhf1o  13035  fvprif  13427  gsumfzz  13579  gsumfzcl  13583  mulgnn  13714  gsumfzreidx  13925  gsumfzsubmcl  13926  gsumfzmptfidmadd  13927  gsumfzmhm  13931  znf1o  14667  dvply1  15491  lgsdir2  15764  lgsne0  15769  gausslemma2dlem1a  15789  gausslemma2dlem1f1o  15791  gausslemma2dlem2  15793  1loopgrvd2fi  16158  1hevtxdg1en  16161  bj-charfun  16405  bj-charfundc  16406  2omap  16597  subctctexmid  16604  nninfsellemeq  16619  nninfsellemeqinf  16621  nninffeq  16625  dcapnconst  16668