Theorem iftrued 3647

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   ifcif 3638

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-if 3639

This theorem is used by:  ifeq2dadc  3672  eqifdc  3677  ifeqeqxdc  3687  mposnif  6185  fimax2gtrilemstep  7209  2omap  7324  updjudhcoinlf  7426  omp1eomlem  7440  difinfsnlem  7445  ctssdclemn0  7456  ctssdc  7459  enumctlemm  7460  nnnninfeq  7474  nninfisollemne  7477  fodju0  7493  nninfwlpoimlemg  7521  nninfwlpoimlemginf  7522  indconst1  9312  iseqf1olemnab  10959  iseqf1olemab  10960  iseqf1olemqk  10965  iseqf1olemfvp  10968  seq3f1olemqsumkj  10969  seq3f1olemqsum  10971  seq3f1oleml  10974  seq3f1o  10975  fser0const  10993  expnnval  11000  swrdval2  11445  swrdlend  11452  swrd0g  11454  2zsupmax  12015  2zinfmin  12034  xrmaxifle  12037  xrmaxiflemab  12038  xrmaxiflemlub  12039  xrmaxiflemcom  12040  summodclem3  12172  summodclem2a  12173  isum  12177  fsum3  12179  isumss  12183  fsumcl2lem  12190  fsumadd  12198  fsummulc2  12240  cvgratz  12324  prodmodclem3  12367  prodmodclem2a  12368  fprodseq  12375  prod1dc  12378  fprodmul  12383  ef0lem  12452  gcdval  12761  nninfctlemfo  12842  pcmpt  13151  pcmpt2  13152  ballotfilemsgt1  13312  ballotfilemsel1i  13314  ballotfilemsi  13316  ennnfonelemss  13359  ennnfonelemkh  13361  ennnfonelemhf1o  13362  fvprif  13723  gzsumcl  13863  mulgnn  13988  gzsumreidx  14231  gzsumsubmcl  14232  gzsummhm  14235  znf1o  15095  dvply1  15991  lgsdir2  16357  lgsne0  16362  gausslemma2dlem1a  16382  gausslemma2dlem1f1o  16384  gausslemma2dlem2  16386  1loopgrvd2fi  16751  1hevtxdg1en  16754  eupth2lem3lem4fi  16919  bj-charfun  17038  bj-charfundc  17039  subctctexmid  17235  idjudju  17252  nninfsellemeq  17263  nninfsellemeqinf  17265  nninffeq  17269  dcapnconst  17318