Theorem iftrued 3609

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 3607	. 2 ⊢ (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1395  ifcif 3602

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 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-if 3603

This theorem is referenced by:  ifeq2dadc  3634  eqifdc  3639  mposnif  6107  fimax2gtrilemstep  7076  updjudhcoinlf  7263  omp1eomlem  7277  difinfsnlem  7282  ctssdclemn0  7293  ctssdc  7296  enumctlemm  7297  nnnninfeq  7311  nninfisollemne  7314  fodju0  7330  nninfwlpoimlemg  7358  nninfwlpoimlemginf  7359  iseqf1olemnab  10740  iseqf1olemab  10741  iseqf1olemqk  10746  iseqf1olemfvp  10749  seq3f1olemqsumkj  10750  seq3f1olemqsum  10752  seq3f1oleml  10755  seq3f1o  10756  fser0const  10774  expnnval  10781  swrdval2  11204  swrdlend  11211  swrd0g  11213  2zsupmax  11758  2zinfmin  11775  xrmaxifle  11778  xrmaxiflemab  11779  xrmaxiflemlub  11780  xrmaxiflemcom  11781  summodclem3  11912  summodclem2a  11913  isum  11917  fsum3  11919  isumss  11923  fsumcl2lem  11930  fsumadd  11938  fsummulc2  11980  cvgratz  12064  prodmodclem3  12107  prodmodclem2a  12108  fprodseq  12115  prod1dc  12118  fprodmul  12123  ef0lem  12192  gcdval  12501  nninfctlemfo  12582  pcmpt  12887  pcmpt2  12888  ennnfonelemss  13002  ennnfonelemkh  13004  ennnfonelemhf1o  13005  fvprif  13397  gsumfzz  13549  gsumfzcl  13553  mulgnn  13684  gsumfzreidx  13895  gsumfzsubmcl  13896  gsumfzmptfidmadd  13897  gsumfzmhm  13901  znf1o  14636  dvply1  15460  lgsdir2  15733  lgsne0  15738  gausslemma2dlem1a  15758  gausslemma2dlem1f1o  15760  gausslemma2dlem2  15762  bj-charfun  16279  bj-charfundc  16280  2omap  16472  subctctexmid  16479  nninfsellemeq  16494  nninfsellemeqinf  16496  nninffeq  16500  dcapnconst  16543