Theorem iftrued 3616

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

Syntax hints:   -> wi 4   = wceq 1398   ifcif 3607

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 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-if 3608

This theorem is referenced by:  ifeq2dadc  3641  eqifdc  3646  mposnif  6125  fimax2gtrilemstep  7133  updjudhcoinlf  7339  omp1eomlem  7353  difinfsnlem  7358  ctssdclemn0  7369  ctssdc  7372  enumctlemm  7373  nnnninfeq  7387  nninfisollemne  7390  fodju0  7406  nninfwlpoimlemg  7434  nninfwlpoimlemginf  7435  iseqf1olemnab  10826  iseqf1olemab  10827  iseqf1olemqk  10832  iseqf1olemfvp  10835  seq3f1olemqsumkj  10836  seq3f1olemqsum  10838  seq3f1oleml  10841  seq3f1o  10842  fser0const  10860  expnnval  10867  swrdval2  11298  swrdlend  11305  swrd0g  11307  2zsupmax  11866  2zinfmin  11883  xrmaxifle  11886  xrmaxiflemab  11887  xrmaxiflemlub  11888  xrmaxiflemcom  11889  summodclem3  12021  summodclem2a  12022  isum  12026  fsum3  12028  isumss  12032  fsumcl2lem  12039  fsumadd  12047  fsummulc2  12089  cvgratz  12173  prodmodclem3  12216  prodmodclem2a  12217  fprodseq  12224  prod1dc  12227  fprodmul  12232  ef0lem  12301  gcdval  12610  nninfctlemfo  12691  pcmpt  12996  pcmpt2  12997  ennnfonelemss  13111  ennnfonelemkh  13113  ennnfonelemhf1o  13114  fvprif  13506  gsumfzz  13658  gsumfzcl  13662  mulgnn  13793  gsumfzreidx  14004  gsumfzsubmcl  14005  gsumfzmptfidmadd  14006  gsumfzmhm  14010  znf1o  14747  dvply1  15576  lgsdir2  15852  lgsne0  15857  gausslemma2dlem1a  15877  gausslemma2dlem1f1o  15879  gausslemma2dlem2  15881  1loopgrvd2fi  16246  1hevtxdg1en  16249  eupth2lem3lem4fi  16414  bj-charfun  16523  bj-charfundc  16524  2omap  16715  subctctexmid  16722  nninfsellemeq  16740  nninfsellemeqinf  16742  nninffeq  16746  dcapnconst  16794