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	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
iftrued	⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)

Proof of Theorem iftrued

Step	Hyp	Ref	Expression
1		iftrued.1	. 2 ⊢ (𝜑 → 𝜒)
2		iftrue 3645	. 2 ⊢ (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1402  ifcif 3638

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 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 theorem 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 referenced by:  ifeq2dadc  3672  eqifdc  3677  ifeqeqxdc  3687  mposnif  6176  fimax2gtrilemstep  7199  2omap  7312  updjudhcoinlf  7414  omp1eomlem  7428  difinfsnlem  7433  ctssdclemn0  7444  ctssdc  7447  enumctlemm  7448  nnnninfeq  7462  nninfisollemne  7465  fodju0  7481  nninfwlpoimlemg  7509  nninfwlpoimlemginf  7510  iseqf1olemnab  10921  iseqf1olemab  10922  iseqf1olemqk  10927  iseqf1olemfvp  10930  seq3f1olemqsumkj  10931  seq3f1olemqsum  10933  seq3f1oleml  10936  seq3f1o  10937  fser0const  10955  expnnval  10962  swrdval2  11406  swrdlend  11413  swrd0g  11415  2zsupmax  11975  2zinfmin  11992  xrmaxifle  11995  xrmaxiflemab  11996  xrmaxiflemlub  11997  xrmaxiflemcom  11998  summodclem3  12130  summodclem2a  12131  isum  12135  fsum3  12137  isumss  12141  fsumcl2lem  12148  fsumadd  12156  fsummulc2  12198  cvgratz  12282  prodmodclem3  12325  prodmodclem2a  12326  fprodseq  12333  prod1dc  12336  fprodmul  12341  ef0lem  12410  gcdval  12719  nninfctlemfo  12800  pcmpt  13105  pcmpt2  13106  ballotfilemsgt1  13237  ballotfilemsel1i  13239  ballotfilemsi  13241  ennnfonelemss  13284  ennnfonelemkh  13286  ennnfonelemhf1o  13287  fvprif  13647  gzsumcl  13787  mulgnn  13912  gzsumreidx  14124  gzsumsubmcl  14125  gzsummhm  14128  znf1o  14969  dvply1  15849  lgsdir2  16135  lgsne0  16140  gausslemma2dlem1a  16160  gausslemma2dlem1f1o  16162  gausslemma2dlem2  16164  1loopgrvd2fi  16529  1hevtxdg1en  16532  eupth2lem3lem4fi  16697  bj-charfun  16816  bj-charfundc  16817  subctctexmid  17013  nninfsellemeq  17031  nninfsellemeqinf  17033  nninffeq  17037  dcapnconst  17085