Theorem iftrued 4490

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4483

This theorem is used by:  partfun  6684  mposnif  7534  tz7.44-3  8409  ttrcltr  9710  updjudhcoinlf  10006  iunfictbso  10186  ttukeylem7  10586  max0sub  13319  ifle  13320  xmulneg1  13392  xmulpnf1  13397  expnnval  14200  swrdval2  14787  swrdlend  14796  swrd0  14801  relexp0g  15168  max0add  15470  summolem2a  15874  prodmolem2a  16094  ef0lem  16237  rpnnen2lem3  16377  rpnnen2lem9  16383  sadadd2lem2  16613  iserodd  17006  pcmpt  17063  pcmpt2  17064  prmdvdsprmo  17213  fvprif  17726  setcepi  18256  gsumval2a  18867  smndex2dlinvh  19109  mgm2nsgrplem3  19112  mulgnn  19278  pmtrprfv  19660  pmtrprfval  19694  psgnunilem1  19700  dfod2  19771  oddvds2  19773  cyggenod  20091  fincygsubgodd  20321  ofldchr  21875  mplcoe1  22339  mplcoe5  22342  coe1tm  22585  coe1tmmul2fv  22590  coe1pwmulfv  22592  coe1sclmul  22594  coe1sclmul2  22596  m1detdiag  22905  mdetunilem9  22928  maducoeval2  22948  symgmatr01lem  22961  pmatcollpw3fi1lem1  23097  chpmat1dlem  23146  chfacffsupp  23167  chfacfscmul0  23169  chfacfpmmul0  23173  2ndcdisj  23768  dscmet  24884  xrsxmet  25122  cnmpopc  25242  xrhmeo  25260  oprpiece1res1  25265  htpycc  25294  pcoval1  25327  pcohtpylem  25333  pcoass  25338  pcorevlem  25340  ovolunlem1a  25810  ovolunlem1  25811  ovolicc2lem3  25833  ovolicc2lem4  25834  mbfi1fseqlem4  26032  mbfi1fseqlem5  26033  mbfi1fseqlem6  26034  itg2const2  26055  itg2splitlem  26062  itg2split  26063  itg2cnlem1  26075  itg2cnlem2  26076  iblss2  26119  itgspliticc  26150  ditgpos  26169  limcres  26199  plyeq0lem  26522  plypf1  26524  coeeq2  26554  dvply1  26598  aareccl  26646  dvtaylp  26690  pserdvlem2  26748  lgamgulmlem4  27352  isppw  27434  vmappw  27436  muval1  27453  dchrelbasd  27559  dchr1  27577  dchrptlem2  27585  lgsdir2  27650  lgsne0  27655  gausslemma2dlem1a  27685  gausslemma2dlem2  27687  2sqnn0  27758  rplogsumlem2  27805  dchrisum0flblem2  27829  dchrisum0fno1  27831  rplogsum  27847  pntrlog2bndlem5  27901  noinfbnd2  28081  expnnsval  28805  angmgmaddov2  29382  1loopgrvd2  30077  1hevtxdg1  30080  1egrvtxdg1  30083  crctcshwlkn0lem2  30393  crctcshlem4  30402  crctcsh  30406  clwlkclwwlklem2fv1  30579  eulercrct  30836  eucrct2eupth  30839  ccatws1f1o  33507  pmtridfv1  33649  pmtridfv2  33650  psgnfzto1stlem  33654  elrgspnlem2  33797  elrgspnlem3  33798  elrspunsn  33972  gsummoncoe1fzo  34122  psrnzr  34137  0mplrim  34139  mplasclco  34141  evlextv  34167  esplyind  34200  vieta  34205  fldextrspunlsp  34299  extdgfialglem2  34318  rtelextdg2lem  34351  2sqr3minply  34405  smattl  34423  smattr  34424  smatbl  34425  1smat1  34429  madjusmdetlem1  34452  madjusmdetlem2  34453  esumpinfval  34698  eulerpartlemgs2  35005  ballotlemsgt1  35136  ballotlemsel1i  35138  ballotlemsi  35140  signswmnd  35179  signsvtn  35206  vonf1oonfo  35877  cvmliftlem10  36038  unblimceq0lem  37352  bj-rdg0gALT  37966  poimirlem1  38519  poimirlem2  38520  poimirlem5  38523  poimirlem6  38524  poimirlem12  38530  poimirlem17  38535  poimirlem19  38537  poimirlem20  38538  poimirlem22  38540  poimirlem23  38541  itg2addnc  38572  itg2gt0cn  38573  itgaddnclem2  38577  sdclem1  38657  cdlemefs27cl  41450  sticksstones9  43184  sticksstones10  43185  sticksstones12a  43187  unitscyglem1  43225  flcidc  44156  oe0suclim  44263  tfsconcatfv  44327  safesnsupfilb  44403  relexp01min  44698  relexpxpmin  44702  mnurnd  45252  ioondisj2  46474  ioondisj1  46475  lptioo1  46613  limsup10exlem  46751  icccncfext  46866  cncfiooicc  46873  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  dvnxpaek  46921  ditgeq3d  46943  itgsubsticclem  46954  dirkerper  47075  dirkercncflem2  47083  fourierdlem40  47126  fourierdlem65  47150  fourierdlem74  47159  fourierdlem75  47160  fourierdlem78  47163  fourierdlem81  47166  fourierdlem97  47182  fourierdlem103  47188  fourierdlem104  47189  sqwvfoura  47207  sqwvfourb  47208  fourierswlem  47209  fouriersw  47210  elaa2lem  47212  etransclem19  47232  etransclem22  47235  etransclem24  47237  etransclem35  47248  sge0pnfval  47352  isomenndlem  47509  hoicvrrex  47535  ovn0  47545  volicon0  47554  hsphoidmvle2  47564  hsphoidmvle  47565  hoidmv1lelem1  47570  hoidmv1lelem2  47571  hoidmvlelem2  47575  hoidmvlelem3  47576  hspmbllem1  47605  hspmbllem2  47606  volico2  47620  ovolval2lem  47622  ovnsubadd2lem  47624  ovolval4lem1  47628  vonioolem1  47659  vonioo  47661  vonicclem1  47662  vonicc  47664  tmachlem-agreeprod  47916  discsubc  50141  oppf1st2nd  50208  2oppf  50209  oppfval  50213