Theorem iftrued 3569

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

Syntax hints:   -> wi 4   = wceq 1364   ifcif 3562

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 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-if 3563

This theorem is referenced by:  ifeq2dadc  3593  eqifdc  3597  mposnif  6020  fimax2gtrilemstep  6970  updjudhcoinlf  7155  omp1eomlem  7169  difinfsnlem  7174  ctssdclemn0  7185  ctssdc  7188  enumctlemm  7189  nnnninfeq  7203  nninfisollemne  7206  fodju0  7222  nninfwlpoimlemg  7250  nninfwlpoimlemginf  7251  iseqf1olemnab  10610  iseqf1olemab  10611  iseqf1olemqk  10616  iseqf1olemfvp  10619  seq3f1olemqsumkj  10620  seq3f1olemqsum  10622  seq3f1oleml  10625  seq3f1o  10626  fser0const  10644  expnnval  10651  2zsupmax  11408  2zinfmin  11425  xrmaxifle  11428  xrmaxiflemab  11429  xrmaxiflemlub  11430  xrmaxiflemcom  11431  summodclem3  11562  summodclem2a  11563  isum  11567  fsum3  11569  isumss  11573  fsumcl2lem  11580  fsumadd  11588  fsummulc2  11630  cvgratz  11714  prodmodclem3  11757  prodmodclem2a  11758  fprodseq  11765  prod1dc  11768  fprodmul  11773  ef0lem  11842  gcdval  12151  nninfctlemfo  12232  pcmpt  12537  pcmpt2  12538  ennnfonelemss  12652  ennnfonelemkh  12654  ennnfonelemhf1o  12655  fvprif  13045  gsumfzz  13197  gsumfzcl  13201  mulgnn  13332  gsumfzreidx  13543  gsumfzsubmcl  13544  gsumfzmptfidmadd  13545  gsumfzmhm  13549  znf1o  14283  dvply1  15085  lgsdir2  15358  lgsne0  15363  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  gausslemma2dlem2  15387  bj-charfun  15537  bj-charfundc  15538  2omap  15726  subctctexmid  15731  nninfsellemeq  15745  nninfsellemeqinf  15747  nninffeq  15751  dcapnconst  15792