Theorem iftrued 3633

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

Syntax hints:   -> wi 4   = wceq 1398   ifcif 3624

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 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-if 3625

This theorem is referenced by:  ifeq2dadc  3658  eqifdc  3663  ifeqeqxdc  3673  mposnif  6155  fimax2gtrilemstep  7171  2omap  7282  updjudhcoinlf  7384  omp1eomlem  7398  difinfsnlem  7403  ctssdclemn0  7414  ctssdc  7417  enumctlemm  7418  nnnninfeq  7432  nninfisollemne  7435  fodju0  7451  nninfwlpoimlemg  7479  nninfwlpoimlemginf  7480  iseqf1olemnab  10887  iseqf1olemab  10888  iseqf1olemqk  10893  iseqf1olemfvp  10896  seq3f1olemqsumkj  10897  seq3f1olemqsum  10899  seq3f1oleml  10902  seq3f1o  10903  fser0const  10921  expnnval  10928  swrdval2  11368  swrdlend  11375  swrd0g  11377  2zsupmax  11936  2zinfmin  11953  xrmaxifle  11956  xrmaxiflemab  11957  xrmaxiflemlub  11958  xrmaxiflemcom  11959  summodclem3  12091  summodclem2a  12092  isum  12096  fsum3  12098  isumss  12102  fsumcl2lem  12109  fsumadd  12117  fsummulc2  12159  cvgratz  12243  prodmodclem3  12286  prodmodclem2a  12287  fprodseq  12294  prod1dc  12297  fprodmul  12302  ef0lem  12371  gcdval  12680  nninfctlemfo  12761  pcmpt  13066  pcmpt2  13067  ballotfilemsgt1  13198  ballotfilemsel1i  13200  ballotfilemsi  13202  ennnfonelemss  13245  ennnfonelemkh  13247  ennnfonelemhf1o  13248  fvprif  13607  gsumfzz  13750  gsumfzcl  13754  mulgnn  13879  gsumfzreidx  14090  gsumfzsubmcl  14091  gsumfzmptfidmadd  14092  gsumfzmhm  14096  znf1o  14925  dvply1  15756  lgsdir2  16032  lgsne0  16037  gausslemma2dlem1a  16057  gausslemma2dlem1f1o  16059  gausslemma2dlem2  16061  1loopgrvd2fi  16426  1hevtxdg1en  16429  eupth2lem3lem4fi  16594  bj-charfun  16703  bj-charfundc  16704  subctctexmid  16900  nninfsellemeq  16918  nninfsellemeqinf  16920  nninffeq  16924  dcapnconst  16973