Theorem iftrued 3533

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

Syntax hints:   -> wi 4   = wceq 1348   ifcif 3526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-if 3527

This theorem is referenced by:  eqifdc  3560  mposnif  5947  fimax2gtrilemstep  6878  updjudhcoinlf  7057  omp1eomlem  7071  difinfsnlem  7076  ctssdclemn0  7087  ctssdc  7090  enumctlemm  7091  nnnninfeq  7104  nninfisollemne  7107  fodju0  7123  nninfwlpoimlemg  7151  nninfwlpoimlemginf  7152  iseqf1olemnab  10444  iseqf1olemab  10445  iseqf1olemqk  10450  iseqf1olemfvp  10453  seq3f1olemqsumkj  10454  seq3f1olemqsum  10456  seq3f1oleml  10459  seq3f1o  10460  fser0const  10472  expnnval  10479  2zsupmax  11189  2zinfmin  11206  xrmaxifle  11209  xrmaxiflemab  11210  xrmaxiflemlub  11211  xrmaxiflemcom  11212  summodclem3  11343  summodclem2a  11344  isum  11348  fsum3  11350  isumss  11354  fsumcl2lem  11361  fsumadd  11369  fsummulc2  11411  cvgratz  11495  prodmodclem3  11538  prodmodclem2a  11539  fprodseq  11546  prod1dc  11549  fprodmul  11554  ef0lem  11623  gcdval  11914  pcmpt  12295  pcmpt2  12296  ennnfonelemss  12365  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ressid2  12477  lgsdir2  13728  lgsne0  13733  bj-charfun  13842  bj-charfundc  13843  subctctexmid  14034  nninfsellemeq  14047  nninfsellemeqinf  14049  nninffeq  14053  dcapnconst  14092