Theorem iftrued 3512

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

Syntax hints:   -> wi 4   = wceq 1335   ifcif 3505

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 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-if 3506

This theorem is referenced by:  eqifdc  3539  mposnif  5912  fimax2gtrilemstep  6842  updjudhcoinlf  7018  omp1eomlem  7032  difinfsnlem  7037  ctssdclemn0  7048  ctssdc  7051  enumctlemm  7052  nnnninfeq  7065  nninfisollemne  7068  fodju0  7084  iseqf1olemnab  10380  iseqf1olemab  10381  iseqf1olemqk  10386  iseqf1olemfvp  10389  seq3f1olemqsumkj  10390  seq3f1olemqsum  10392  seq3f1oleml  10395  seq3f1o  10396  fser0const  10408  expnnval  10415  2zsupmax  11118  xrmaxifle  11136  xrmaxiflemab  11137  xrmaxiflemlub  11138  xrmaxiflemcom  11139  summodclem3  11270  summodclem2a  11271  isum  11275  fsum3  11277  isumss  11281  fsumcl2lem  11288  fsumadd  11296  fsummulc2  11338  cvgratz  11422  prodmodclem3  11465  prodmodclem2a  11466  fprodseq  11473  prod1dc  11476  fprodmul  11481  ef0lem  11550  gcdval  11834  ennnfonelemss  12122  ennnfonelemkh  12124  ennnfonelemhf1o  12125  ressid2  12220  bj-charfun  13353  bj-charfundc  13354  subctctexmid  13544  nninfsellemeq  13557  nninfsellemeqinf  13559  nninffeq  13563  dcapnconst  13602