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  6118  fimax2gtrilemstep  7093  updjudhcoinlf  7282  omp1eomlem  7296  difinfsnlem  7301  ctssdclemn0  7312  ctssdc  7315  enumctlemm  7316  nnnninfeq  7330  nninfisollemne  7333  fodju0  7349  nninfwlpoimlemg  7377  nninfwlpoimlemginf  7378  iseqf1olemnab  10767  iseqf1olemab  10768  iseqf1olemqk  10773  iseqf1olemfvp  10776  seq3f1olemqsumkj  10777  seq3f1olemqsum  10779  seq3f1oleml  10782  seq3f1o  10783  fser0const  10801  expnnval  10808  swrdval2  11239  swrdlend  11246  swrd0g  11248  2zsupmax  11807  2zinfmin  11824  xrmaxifle  11827  xrmaxiflemab  11828  xrmaxiflemlub  11829  xrmaxiflemcom  11830  summodclem3  11962  summodclem2a  11963  isum  11967  fsum3  11969  isumss  11973  fsumcl2lem  11980  fsumadd  11988  fsummulc2  12030  cvgratz  12114  prodmodclem3  12157  prodmodclem2a  12158  fprodseq  12165  prod1dc  12168  fprodmul  12173  ef0lem  12242  gcdval  12551  nninfctlemfo  12632  pcmpt  12937  pcmpt2  12938  ennnfonelemss  13052  ennnfonelemkh  13054  ennnfonelemhf1o  13055  fvprif  13447  gsumfzz  13599  gsumfzcl  13603  mulgnn  13734  gsumfzreidx  13945  gsumfzsubmcl  13946  gsumfzmptfidmadd  13947  gsumfzmhm  13951  znf1o  14687  dvply1  15516  lgsdir2  15789  lgsne0  15794  gausslemma2dlem1a  15814  gausslemma2dlem1f1o  15816  gausslemma2dlem2  15818  1loopgrvd2fi  16183  1hevtxdg1en  16186  eupth2lem3lem4fi  16351  bj-charfun  16461  bj-charfundc  16462  2omap  16653  subctctexmid  16660  nninfsellemeq  16675  nninfsellemeqinf  16677  nninffeq  16681  dcapnconst  16725