Theorem iftrued 3609

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

Syntax hints:   -> wi 4   = wceq 1395   ifcif 3602

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 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-if 3603

This theorem is referenced by:  ifeq2dadc  3634  eqifdc  3639  mposnif  6097  fimax2gtrilemstep  7058  updjudhcoinlf  7243  omp1eomlem  7257  difinfsnlem  7262  ctssdclemn0  7273  ctssdc  7276  enumctlemm  7277  nnnninfeq  7291  nninfisollemne  7294  fodju0  7310  nninfwlpoimlemg  7338  nninfwlpoimlemginf  7339  iseqf1olemnab  10718  iseqf1olemab  10719  iseqf1olemqk  10724  iseqf1olemfvp  10727  seq3f1olemqsumkj  10728  seq3f1olemqsum  10730  seq3f1oleml  10733  seq3f1o  10734  fser0const  10752  expnnval  10759  swrdval2  11178  swrdlend  11185  swrd0g  11187  2zsupmax  11732  2zinfmin  11749  xrmaxifle  11752  xrmaxiflemab  11753  xrmaxiflemlub  11754  xrmaxiflemcom  11755  summodclem3  11886  summodclem2a  11887  isum  11891  fsum3  11893  isumss  11897  fsumcl2lem  11904  fsumadd  11912  fsummulc2  11954  cvgratz  12038  prodmodclem3  12081  prodmodclem2a  12082  fprodseq  12089  prod1dc  12092  fprodmul  12097  ef0lem  12166  gcdval  12475  nninfctlemfo  12556  pcmpt  12861  pcmpt2  12862  ennnfonelemss  12976  ennnfonelemkh  12978  ennnfonelemhf1o  12979  fvprif  13371  gsumfzz  13523  gsumfzcl  13527  mulgnn  13658  gsumfzreidx  13869  gsumfzsubmcl  13870  gsumfzmptfidmadd  13871  gsumfzmhm  13875  znf1o  14609  dvply1  15433  lgsdir2  15706  lgsne0  15711  gausslemma2dlem1a  15731  gausslemma2dlem1f1o  15733  gausslemma2dlem2  15735  bj-charfun  16128  bj-charfundc  16129  2omap  16318  subctctexmid  16325  nninfsellemeq  16339  nninfsellemeqinf  16341  nninffeq  16345  dcapnconst  16388