Theorem iftrued 3565

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 3563	. 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 3558

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-if 3559

This theorem is referenced by:  ifeq2dadc  3589  eqifdc  3593  mposnif  6013  fimax2gtrilemstep  6958  updjudhcoinlf  7141  omp1eomlem  7155  difinfsnlem  7160  ctssdclemn0  7171  ctssdc  7174  enumctlemm  7175  nnnninfeq  7189  nninfisollemne  7192  fodju0  7208  nninfwlpoimlemg  7236  nninfwlpoimlemginf  7237  iseqf1olemnab  10575  iseqf1olemab  10576  iseqf1olemqk  10581  iseqf1olemfvp  10584  seq3f1olemqsumkj  10585  seq3f1olemqsum  10587  seq3f1oleml  10590  seq3f1o  10591  fser0const  10609  expnnval  10616  2zsupmax  11372  2zinfmin  11389  xrmaxifle  11392  xrmaxiflemab  11393  xrmaxiflemlub  11394  xrmaxiflemcom  11395  summodclem3  11526  summodclem2a  11527  isum  11531  fsum3  11533  isumss  11537  fsumcl2lem  11544  fsumadd  11552  fsummulc2  11594  cvgratz  11678  prodmodclem3  11721  prodmodclem2a  11722  fprodseq  11729  prod1dc  11732  fprodmul  11737  ef0lem  11806  gcdval  12099  nninfctlemfo  12180  pcmpt  12484  pcmpt2  12485  ennnfonelemss  12570  ennnfonelemkh  12572  ennnfonelemhf1o  12573  fvprif  12929  gsumfzz  13070  gsumfzcl  13074  mulgnn  13199  gsumfzreidx  13410  gsumfzsubmcl  13411  gsumfzmptfidmadd  13412  gsumfzmhm  13416  znf1o  14150  dvply1  14943  lgsdir2  15190  lgsne0  15195  gausslemma2dlem1a  15215  gausslemma2dlem1f1o  15217  gausslemma2dlem2  15219  bj-charfun  15369  bj-charfundc  15370  subctctexmid  15561  nninfsellemeq  15574  nninfsellemeqinf  15576  nninffeq  15580  dcapnconst  15621