Theorem iftrued 3542

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

Syntax hints:   -> wi 4   = wceq 1353   ifcif 3535

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 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-if 3536

This theorem is referenced by:  ifeq2dadc  3566  eqifdc  3570  mposnif  5969  fimax2gtrilemstep  6900  updjudhcoinlf  7079  omp1eomlem  7093  difinfsnlem  7098  ctssdclemn0  7109  ctssdc  7112  enumctlemm  7113  nnnninfeq  7126  nninfisollemne  7129  fodju0  7145  nninfwlpoimlemg  7173  nninfwlpoimlemginf  7174  iseqf1olemnab  10488  iseqf1olemab  10489  iseqf1olemqk  10494  iseqf1olemfvp  10497  seq3f1olemqsumkj  10498  seq3f1olemqsum  10500  seq3f1oleml  10503  seq3f1o  10504  fser0const  10516  expnnval  10523  2zsupmax  11234  2zinfmin  11251  xrmaxifle  11254  xrmaxiflemab  11255  xrmaxiflemlub  11256  xrmaxiflemcom  11257  summodclem3  11388  summodclem2a  11389  isum  11393  fsum3  11395  isumss  11399  fsumcl2lem  11406  fsumadd  11414  fsummulc2  11456  cvgratz  11540  prodmodclem3  11583  prodmodclem2a  11584  fprodseq  11591  prod1dc  11594  fprodmul  11599  ef0lem  11668  gcdval  11960  pcmpt  12341  pcmpt2  12342  ennnfonelemss  12411  ennnfonelemkh  12413  ennnfonelemhf1o  12414  fvprif  12762  mulgnn  12989  lgsdir2  14437  lgsne0  14442  bj-charfun  14562  bj-charfundc  14563  subctctexmid  14753  nninfsellemeq  14766  nninfsellemeqinf  14768  nninffeq  14772  dcapnconst  14811