Theorem iftrued 4487

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

Syntax hints:   → wi 4   = wceq 1541  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4480

This theorem is referenced by:  partfun  6639  mposnif  7474  tz7.44-3  8339  ttrcltr  9625  updjudhcoinlf  9844  iunfictbso  10024  ttukeylem7  10425  max0sub  13111  ifle  13112  xmulneg1  13184  xmulpnf1  13189  expnnval  13987  swrdval2  14570  swrdlend  14577  swrd0  14582  relexp0g  14945  max0add  15233  summolem2a  15638  prodmolem2a  15857  ef0lem  16001  rpnnen2lem3  16141  rpnnen2lem9  16147  iserodd  16763  pcmpt  16820  pcmpt2  16821  prmdvdsprmo  16970  fvprif  17482  setcepi  18012  gsumval2a  18610  smndex2dlinvh  18842  mgm2nsgrplem3  18845  mulgnn  19005  pmtrprfv  19382  pmtrprfval  19416  psgnunilem1  19422  dfod2  19493  oddvds2  19495  cyggenod  19813  fincygsubgodd  20043  ofldchr  21531  mplcoe1  21992  mplcoe5  21995  coe1tm  22215  coe1tmmul2fv  22220  coe1pwmulfv  22222  coe1sclmul  22224  coe1sclmul2  22226  m1detdiag  22541  mdetunilem9  22564  maducoeval2  22584  symgmatr01lem  22597  pmatcollpw3fi1lem1  22730  chpmat1dlem  22779  chfacffsupp  22800  chfacfscmul0  22802  chfacfpmmul0  22806  2ndcdisj  23400  dscmet  24516  xrsxmet  24754  cnmpopc  24878  xrhmeo  24900  oprpiece1res1  24905  htpycc  24935  pcoval1  24969  pcohtpylem  24975  pcoass  24980  pcorevlem  24982  ovolunlem1a  25453  ovolunlem1  25454  ovolicc2lem3  25476  ovolicc2lem4  25477  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  mbfi1fseqlem6  25677  itg2const2  25698  itg2splitlem  25705  itg2split  25706  itg2cnlem1  25718  itg2cnlem2  25719  iblss2  25763  itgspliticc  25794  ditgpos  25813  limcres  25843  plyeq0lem  26171  plypf1  26173  coeeq2  26203  dvply1  26247  aareccl  26290  dvtaylp  26334  pserdvlem2  26394  lgamgulmlem4  26998  isppw  27080  vmappw  27082  muval1  27099  dchrelbasd  27206  dchr1  27224  dchrptlem2  27232  lgsdir2  27297  lgsne0  27302  gausslemma2dlem1a  27332  gausslemma2dlem2  27334  2sqnn0  27405  rplogsumlem2  27452  dchrisum0flblem2  27476  dchrisum0fno1  27478  rplogsum  27494  pntrlog2bndlem5  27548  noinfbnd2  27699  expnnsval  28422  1loopgrvd2  29577  1hevtxdg1  29580  1egrvtxdg1  29583  crctcshwlkn0lem2  29884  crctcshlem4  29893  crctcsh  29897  clwlkclwwlklem2fv1  30070  eulercrct  30317  eucrct2eupth  30320  ccatws1f1o  33033  pmtridfv1  33177  pmtridfv2  33178  psgnfzto1stlem  33182  elrgspnlem2  33325  elrgspnlem3  33326  elrspunsn  33510  gsummoncoe1fzo  33678  evlextv  33707  esplyind  33731  vieta  33736  fldextrspunlsp  33831  extdgfialglem2  33850  rtelextdg2lem  33883  2sqr3minply  33937  smattl  33955  smattr  33956  smatbl  33957  1smat1  33961  madjusmdetlem1  33984  madjusmdetlem2  33985  esumpinfval  34230  eulerpartlemgs2  34537  ballotlemsgt1  34668  ballotlemsel1i  34670  ballotlemsi  34672  signswmnd  34714  signsvtn  34741  cvmliftlem10  35488  unblimceq0lem  36706  bj-rdg0gALT  37272  poimirlem1  37818  poimirlem2  37819  poimirlem5  37822  poimirlem6  37823  poimirlem12  37829  poimirlem17  37834  poimirlem19  37836  poimirlem20  37837  poimirlem22  37839  poimirlem23  37840  itg2addnc  37871  itg2gt0cn  37872  itgaddnclem2  37876  sdclem1  37940  cdlemefs27cl  40669  sticksstones9  42404  sticksstones10  42405  sticksstones12a  42407  unitscyglem1  42445  flcidc  43408  oe0suclim  43515  tfsconcatfv  43579  safesnsupfilb  43655  relexp01min  43950  relexpxpmin  43954  mnurnd  44520  ioondisj2  45735  ioondisj1  45736  lptioo1  45874  limsup10exlem  46012  icccncfext  46127  cncfiooicc  46134  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  dvnxpaek  46182  ditgeq3d  46204  itgsubsticclem  46215  dirkerper  46336  dirkercncflem2  46344  fourierdlem40  46387  fourierdlem65  46411  fourierdlem74  46420  fourierdlem75  46421  fourierdlem78  46424  fourierdlem81  46427  fourierdlem97  46443  fourierdlem103  46449  fourierdlem104  46450  sqwvfoura  46468  sqwvfourb  46469  fourierswlem  46470  fouriersw  46471  elaa2lem  46473  etransclem19  46493  etransclem22  46496  etransclem24  46498  etransclem35  46509  sge0pnfval  46613  isomenndlem  46770  hoicvrrex  46796  ovn0  46806  volicon0  46815  hsphoidmvle2  46825  hsphoidmvle  46826  hoidmv1lelem1  46831  hoidmv1lelem2  46832  hoidmvlelem2  46836  hoidmvlelem3  46837  hspmbllem1  46866  hspmbllem2  46867  volico2  46881  ovolval2lem  46883  ovnsubadd2lem  46885  ovolval4lem1  46889  vonioolem1  46920  vonioo  46922  vonicclem1  46923  vonicc  46925  discsubc  49305  oppf1st2nd  49372  2oppf  49373  oppfval  49377