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  6104  fimax2gtrilemstep  7071  updjudhcoinlf  7258  omp1eomlem  7272  difinfsnlem  7277  ctssdclemn0  7288  ctssdc  7291  enumctlemm  7292  nnnninfeq  7306  nninfisollemne  7309  fodju0  7325  nninfwlpoimlemg  7353  nninfwlpoimlemginf  7354  iseqf1olemnab  10735  iseqf1olemab  10736  iseqf1olemqk  10741  iseqf1olemfvp  10744  seq3f1olemqsumkj  10745  seq3f1olemqsum  10747  seq3f1oleml  10750  seq3f1o  10751  fser0const  10769  expnnval  10776  swrdval2  11198  swrdlend  11205  swrd0g  11207  2zsupmax  11752  2zinfmin  11769  xrmaxifle  11772  xrmaxiflemab  11773  xrmaxiflemlub  11774  xrmaxiflemcom  11775  summodclem3  11906  summodclem2a  11907  isum  11911  fsum3  11913  isumss  11917  fsumcl2lem  11924  fsumadd  11932  fsummulc2  11974  cvgratz  12058  prodmodclem3  12101  prodmodclem2a  12102  fprodseq  12109  prod1dc  12112  fprodmul  12117  ef0lem  12186  gcdval  12495  nninfctlemfo  12576  pcmpt  12881  pcmpt2  12882  ennnfonelemss  12996  ennnfonelemkh  12998  ennnfonelemhf1o  12999  fvprif  13391  gsumfzz  13543  gsumfzcl  13547  mulgnn  13678  gsumfzreidx  13889  gsumfzsubmcl  13890  gsumfzmptfidmadd  13891  gsumfzmhm  13895  znf1o  14630  dvply1  15454  lgsdir2  15727  lgsne0  15732  gausslemma2dlem1a  15752  gausslemma2dlem1f1o  15754  gausslemma2dlem2  15756  bj-charfun  16225  bj-charfundc  16226  2omap  16418  subctctexmid  16425  nninfsellemeq  16440  nninfsellemeqinf  16442  nninffeq  16446  dcapnconst  16489