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  6114  fimax2gtrilemstep  7089  updjudhcoinlf  7278  omp1eomlem  7292  difinfsnlem  7297  ctssdclemn0  7308  ctssdc  7311  enumctlemm  7312  nnnninfeq  7326  nninfisollemne  7329  fodju0  7345  nninfwlpoimlemg  7373  nninfwlpoimlemginf  7374  iseqf1olemnab  10762  iseqf1olemab  10763  iseqf1olemqk  10768  iseqf1olemfvp  10771  seq3f1olemqsumkj  10772  seq3f1olemqsum  10774  seq3f1oleml  10777  seq3f1o  10778  fser0const  10796  expnnval  10803  swrdval2  11231  swrdlend  11238  swrd0g  11240  2zsupmax  11786  2zinfmin  11803  xrmaxifle  11806  xrmaxiflemab  11807  xrmaxiflemlub  11808  xrmaxiflemcom  11809  summodclem3  11940  summodclem2a  11941  isum  11945  fsum3  11947  isumss  11951  fsumcl2lem  11958  fsumadd  11966  fsummulc2  12008  cvgratz  12092  prodmodclem3  12135  prodmodclem2a  12136  fprodseq  12143  prod1dc  12146  fprodmul  12151  ef0lem  12220  gcdval  12529  nninfctlemfo  12610  pcmpt  12915  pcmpt2  12916  ennnfonelemss  13030  ennnfonelemkh  13032  ennnfonelemhf1o  13033  fvprif  13425  gsumfzz  13577  gsumfzcl  13581  mulgnn  13712  gsumfzreidx  13923  gsumfzsubmcl  13924  gsumfzmptfidmadd  13925  gsumfzmhm  13929  znf1o  14664  dvply1  15488  lgsdir2  15761  lgsne0  15766  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  gausslemma2dlem2  15790  1loopgrvd2fi  16155  1hevtxdg1en  16158  bj-charfun  16402  bj-charfundc  16403  2omap  16594  subctctexmid  16601  nninfsellemeq  16616  nninfsellemeqinf  16618  nninffeq  16622  dcapnconst  16665