Theorem iftrued 4489

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  partfun  6687  mposnif  7537  tz7.44-3  8420  ttrcltr  9721  updjudhcoinlf  10017  iunfictbso  10197  ttukeylem7  10597  max0sub  13330  ifle  13331  xmulneg1  13403  xmulpnf1  13408  expnnval  14211  swrdval2  14799  swrdlend  14808  swrd0  14813  relexp0g  15181  max0add  15483  summolem2a  15887  prodmolem2a  16107  ef0lem  16250  rpnnen2lem3  16390  rpnnen2lem9  16396  sadadd2lem2  16626  iserodd  17019  pcmpt  17076  pcmpt2  17077  prmdvdsprmo  17226  fvprif  17739  setcepi  18269  gsumval2a  18880  smndex2dlinvh  19122  mgm2nsgrplem3  19125  mulgnn  19291  pmtrprfv  19673  pmtrprfval  19707  psgnunilem1  19713  dfod2  19784  oddvds2  19786  cyggenod  20104  fincygsubgodd  20334  ofldchr  21888  mplcoe1  22352  mplcoe5  22355  coe1tm  22598  coe1tmmul2fv  22603  coe1pwmulfv  22605  coe1sclmul  22607  coe1sclmul2  22609  m1detdiag  22918  mdetunilem9  22941  maducoeval2  22961  symgmatr01lem  22974  pmatcollpw3fi1lem1  23110  chpmat1dlem  23159  chfacffsupp  23180  chfacfscmul0  23182  chfacfpmmul0  23186  2ndcdisj  23781  dscmet  24897  xrsxmet  25135  cnmpopc  25255  xrhmeo  25273  oprpiece1res1  25278  htpycc  25307  pcoval1  25340  pcohtpylem  25346  pcoass  25351  pcorevlem  25353  ovolunlem1a  25823  ovolunlem1  25824  ovolicc2lem3  25846  ovolicc2lem4  25847  mbfi1fseqlem4  26045  mbfi1fseqlem5  26046  mbfi1fseqlem6  26047  itg2const2  26068  itg2splitlem  26075  itg2split  26076  itg2cnlem1  26088  itg2cnlem2  26089  iblss2  26132  itgspliticc  26163  ditgpos  26182  limcres  26212  plyeq0lem  26535  plypf1  26537  coeeq2  26567  dvply1  26611  aareccl  26659  dvtaylp  26703  pserdvlem2  26761  lgamgulmlem4  27365  isppw  27447  vmappw  27449  muval1  27466  dchrelbasd  27572  dchr1  27590  dchrptlem2  27598  lgsdir2  27663  lgsne0  27668  gausslemma2dlem1a  27698  gausslemma2dlem2  27700  2sqnn0  27771  rplogsumlem2  27818  dchrisum0flblem2  27842  dchrisum0fno1  27844  rplogsum  27860  pntrlog2bndlem5  27914  noinfbnd2  28094  expnnsval  28818  angmgmaddov2  29395  1loopgrvd2  30090  1hevtxdg1  30093  1egrvtxdg1  30096  crctcshwlkn0lem2  30406  crctcshlem4  30415  crctcsh  30419  clwlkclwwlklem2fv1  30592  eulercrct  30849  eucrct2eupth  30852  ccatws1f1o  33561  pmtridfv1  33703  pmtridfv2  33704  psgnfzto1stlem  33708  elrgspnlem2  33851  elrgspnlem3  33852  elrspunsn  34026  gsummoncoe1fzo  34176  psrnzr  34191  0mplrim  34193  mplasclco  34195  evlextv  34221  esplyind  34254  vieta  34259  fldextrspunlsp  34353  extdgfialglem2  34372  rtelextdg2lem  34405  2sqr3minply  34459  smattl  34477  smattr  34478  smatbl  34479  1smat1  34483  madjusmdetlem1  34506  madjusmdetlem2  34507  esumpinfval  34752  eulerpartlemgs2  35059  ballotlemsgt1  35190  ballotlemsel1i  35192  ballotlemsi  35194  signswmnd  35233  signsvtn  35260  vonf1oonfo  35969  cvmliftlem10  36146  unblimceq0lem  37465  bj-rdg0gALT  38079  poimirlem1  38633  poimirlem2  38634  poimirlem5  38637  poimirlem6  38638  poimirlem12  38644  poimirlem17  38649  poimirlem19  38651  poimirlem20  38652  poimirlem22  38654  poimirlem23  38655  itg2addnc  38686  itg2gt0cn  38687  itgaddnclem2  38691  sdclem1  38771  cdlemefs27cl  41564  sticksstones9  43298  sticksstones10  43299  sticksstones12a  43301  unitscyglem1  43339  flcidc  44266  oe0suclim  44373  tfsconcatfv  44437  safesnsupfilb  44513  relexp01min  44807  relexpxpmin  44811  mnurnd  45361  ioondisj2  46599  ioondisj1  46600  lptioo1  46738  limsup10exlem  46876  icccncfext  46991  cncfiooicc  46998  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  dvnxpaek  47046  ditgeq3d  47068  itgsubsticclem  47079  dirkerper  47200  dirkercncflem2  47208  fourierdlem40  47251  fourierdlem65  47275  fourierdlem74  47284  fourierdlem75  47285  fourierdlem78  47288  fourierdlem81  47291  fourierdlem97  47307  fourierdlem103  47313  fourierdlem104  47314  sqwvfoura  47332  sqwvfourb  47333  fourierswlem  47334  fouriersw  47335  elaa2lem  47337  etransclem19  47357  etransclem22  47360  etransclem24  47362  etransclem35  47373  sge0pnfval  47477  isomenndlem  47634  hoicvrrex  47660  ovn0  47670  volicon0  47679  hsphoidmvle2  47689  hsphoidmvle  47690  hoidmv1lelem1  47695  hoidmv1lelem2  47696  hoidmvlelem2  47700  hoidmvlelem3  47701  hspmbllem1  47730  hspmbllem2  47731  volico2  47745  ovolval2lem  47747  ovnsubadd2lem  47749  ovolval4lem1  47753  vonioolem1  47784  vonioo  47786  vonicclem1  47787  vonicc  47789  tmachlem-agreeprod  48041  discsubc  50272  oppf1st2nd  50341  2oppf  50342  oppfval  50346  parhomidval  50840  parhomideq2  50843  parcoval2  50860  parmapcl  50865