Theorem iftrued 3543

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 3541	. 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 3536

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 3537

This theorem is referenced by:  ifeq2dadc  3567  eqifdc  3571  mposnif  5971  fimax2gtrilemstep  6902  updjudhcoinlf  7081  omp1eomlem  7095  difinfsnlem  7100  ctssdclemn0  7111  ctssdc  7114  enumctlemm  7115  nnnninfeq  7128  nninfisollemne  7131  fodju0  7147  nninfwlpoimlemg  7175  nninfwlpoimlemginf  7176  iseqf1olemnab  10490  iseqf1olemab  10491  iseqf1olemqk  10496  iseqf1olemfvp  10499  seq3f1olemqsumkj  10500  seq3f1olemqsum  10502  seq3f1oleml  10505  seq3f1o  10506  fser0const  10518  expnnval  10525  2zsupmax  11236  2zinfmin  11253  xrmaxifle  11256  xrmaxiflemab  11257  xrmaxiflemlub  11258  xrmaxiflemcom  11259  summodclem3  11390  summodclem2a  11391  isum  11395  fsum3  11397  isumss  11401  fsumcl2lem  11408  fsumadd  11416  fsummulc2  11458  cvgratz  11542  prodmodclem3  11585  prodmodclem2a  11586  fprodseq  11593  prod1dc  11596  fprodmul  11601  ef0lem  11670  gcdval  11962  pcmpt  12343  pcmpt2  12344  ennnfonelemss  12413  ennnfonelemkh  12415  ennnfonelemhf1o  12416  fvprif  12767  mulgnn  12994  lgsdir2  14473  lgsne0  14478  bj-charfun  14598  bj-charfundc  14599  subctctexmid  14789  nninfsellemeq  14802  nninfsellemeqinf  14804  nninffeq  14808  dcapnconst  14848