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 1559  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4480

This theorem is referenced by:  partfun  6664  mposnif  7508  tz7.44-3  8374  ttrcltr  9668  updjudhcoinlf  9887  iunfictbso  10067  ttukeylem7  10469  max0sub  13196  ifle  13197  xmulneg1  13269  xmulpnf1  13274  expnnval  14074  swrdval2  14657  swrdlend  14664  swrd0  14669  relexp0g  15032  max0add  15320  summolem2a  15725  prodmolem2a  15947  ef0lem  16091  rpnnen2lem3  16231  rpnnen2lem9  16237  iserodd  16854  pcmpt  16911  pcmpt2  16912  prmdvdsprmo  17061  fvprif  17574  setcepi  18104  gsumval2a  18702  smndex2dlinvh  18937  mgm2nsgrplem3  18940  mulgnn  19100  pmtrprfv  19476  pmtrprfval  19510  psgnunilem1  19516  dfod2  19587  oddvds2  19589  cyggenod  19907  fincygsubgodd  20137  ofldchr  21608  mplcoe1  22070  mplcoe5  22073  coe1tm  22316  coe1tmmul2fv  22321  coe1pwmulfv  22323  coe1sclmul  22325  coe1sclmul2  22327  m1detdiag  22637  mdetunilem9  22660  maducoeval2  22680  symgmatr01lem  22693  pmatcollpw3fi1lem1  22826  chpmat1dlem  22875  chfacffsupp  22896  chfacfscmul0  22898  chfacfpmmul0  22902  2ndcdisj  23496  dscmet  24612  xrsxmet  24850  cnmpopc  24970  xrhmeo  24988  oprpiece1res1  24993  htpycc  25022  pcoval1  25055  pcohtpylem  25061  pcoass  25066  pcorevlem  25068  ovolunlem1a  25538  ovolunlem1  25539  ovolicc2lem3  25561  ovolicc2lem4  25562  mbfi1fseqlem4  25760  mbfi1fseqlem5  25761  mbfi1fseqlem6  25762  itg2const2  25783  itg2splitlem  25790  itg2split  25791  itg2cnlem1  25803  itg2cnlem2  25804  iblss2  25848  itgspliticc  25879  ditgpos  25898  limcres  25928  plyeq0lem  26250  plypf1  26252  coeeq2  26282  dvply1  26325  aareccl  26367  dvtaylp  26410  pserdvlem2  26468  lgamgulmlem4  27073  isppw  27155  vmappw  27157  muval1  27174  dchrelbasd  27280  dchr1  27298  dchrptlem2  27306  lgsdir2  27371  lgsne0  27376  gausslemma2dlem1a  27406  gausslemma2dlem2  27408  2sqnn0  27479  rplogsumlem2  27526  dchrisum0flblem2  27550  dchrisum0fno1  27552  rplogsum  27568  pntrlog2bndlem5  27622  noinfbnd2  27772  expnnsval  28496  1loopgrvd2  29650  1hevtxdg1  29653  1egrvtxdg1  29656  crctcshwlkn0lem2  29957  crctcshlem4  29966  crctcsh  29970  clwlkclwwlklem2fv1  30143  eulercrct  30390  eucrct2eupth  30393  ccatws1f1o  33090  pmtridfv1  33236  pmtridfv2  33237  psgnfzto1stlem  33241  elrgspnlem2  33385  elrgspnlem3  33386  elrspunsn  33576  gsummoncoe1fzo  33754  psrnzr  33770  0mplrim  33772  mplasclco  33774  evlextv  33800  esplyind  33833  vieta  33838  fldextrspunlsp  33932  extdgfialglem2  33951  rtelextdg2lem  33984  2sqr3minply  34038  smattl  34056  smattr  34057  smatbl  34058  1smat1  34062  madjusmdetlem1  34085  madjusmdetlem2  34086  esumpinfval  34331  eulerpartlemgs2  34638  ballotlemsgt1  34769  ballotlemsel1i  34771  ballotlemsi  34773  signswmnd  34815  signsvtn  34842  vonf1oonfo  35422  cvmliftlem10  35608  unblimceq0lem  36908  bj-rdg0gALT  37520  poimirlem1  38084  poimirlem2  38085  poimirlem5  38088  poimirlem6  38089  poimirlem12  38095  poimirlem17  38100  poimirlem19  38102  poimirlem20  38103  poimirlem22  38105  poimirlem23  38106  itg2addnc  38137  itg2gt0cn  38138  itgaddnclem2  38142  sdclem1  38206  cdlemefs27cl  41001  sticksstones9  42735  sticksstones10  42736  sticksstones12a  42738  unitscyglem1  42776  flcidc  43711  oe0suclim  43818  tfsconcatfv  43882  safesnsupfilb  43958  relexp01min  44253  relexpxpmin  44257  mnurnd  44823  ioondisj2  46033  ioondisj1  46034  lptioo1  46172  limsup10exlem  46310  icccncfext  46425  cncfiooicc  46432  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  dvnxpaek  46480  ditgeq3d  46502  itgsubsticclem  46513  dirkerper  46634  dirkercncflem2  46642  fourierdlem40  46685  fourierdlem65  46709  fourierdlem74  46718  fourierdlem75  46719  fourierdlem78  46722  fourierdlem81  46725  fourierdlem97  46741  fourierdlem103  46747  fourierdlem104  46748  sqwvfoura  46766  sqwvfourb  46767  fourierswlem  46768  fouriersw  46769  elaa2lem  46771  etransclem19  46791  etransclem22  46794  etransclem24  46796  etransclem35  46807  sge0pnfval  46911  isomenndlem  47068  hoicvrrex  47094  ovn0  47104  volicon0  47113  hsphoidmvle2  47123  hsphoidmvle  47124  hoidmv1lelem1  47129  hoidmv1lelem2  47130  hoidmvlelem2  47134  hoidmvlelem3  47135  hspmbllem1  47164  hspmbllem2  47165  volico2  47179  ovolval2lem  47181  ovnsubadd2lem  47183  ovolval4lem1  47187  vonioolem1  47218  vonioo  47220  vonicclem1  47221  vonicc  47223  discsubc  49649  oppf1st2nd  49716  2oppf  49717  oppfval  49721