Theorem iftrued 4395

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

Syntax hints:   → wi 4   = wceq 1525  ifcif 4387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ex 1766  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-if 4388

This theorem is referenced by:  mposnif  7131  tz7.44-3  7903  updjudhcoinlf  9214  iunfictbso  9393  ttukeylem7  9790  max0sub  12443  ifle  12444  xmulneg1  12516  xmulpnf1  12521  expnnval  13286  swrdval2  13848  swrdlend  13855  swrd0  13860  relexp0g  14219  max0add  14508  summolem2a  14909  prodmolem2a  15125  ef0lem  15269  rpnnen2lem3  15406  rpnnen2lem9  15412  iserodd  16005  pcmpt  16061  pcmpt2  16062  prmdvdsprmo  16211  fvprif  16667  setcepi  17181  gsumval2a  17722  mgm2nsgrplem3  17850  mulgnn  17993  pmtrprfv  18316  pmtrprfval  18350  psgnunilem1  18356  dfod2  18425  oddvds2  18427  cyggenod  18730  mplcoe1  19937  mplcoe5  19940  coe1tm  20128  coe1tmmul2fv  20133  coe1pwmulfv  20135  coe1sclmul  20137  coe1sclmul2  20139  m1detdiag  20894  mdetunilem9  20917  maducoeval2  20937  symgmatr01lem  20950  pmatcollpw3fi1lem1  21082  chpmat1dlem  21131  chfacffsupp  21152  chfacfscmul0  21154  chfacfpmmul0  21158  2ndcdisj  21752  dscmet  22869  xrsxmet  23104  cnmpopc  23219  xrhmeo  23237  oprpiece1res1  23242  htpycc  23271  pcoval1  23304  pcohtpylem  23310  pcoass  23315  pcorevlem  23317  ovolunlem1a  23784  ovolunlem1  23785  ovolicc2lem3  23807  ovolicc2lem4  23808  mbfi1fseqlem4  24006  mbfi1fseqlem5  24007  mbfi1fseqlem6  24008  itg2const2  24029  itg2splitlem  24036  itg2split  24037  itg2cnlem1  24049  itg2cnlem2  24050  iblss2  24093  itgspliticc  24124  ditgpos  24141  limcres  24171  plyeq0lem  24487  plypf1  24489  coeeq2  24519  dvply1  24560  aareccl  24602  dvtaylp  24645  pserdvlem2  24703  lgamgulmlem4  25295  isppw  25377  vmappw  25379  muval1  25396  dchrelbasd  25501  dchr1  25519  dchrptlem2  25527  lgsdir2  25592  lgsne0  25597  gausslemma2dlem1a  25627  gausslemma2dlem2  25629  2sqnn0  25700  rplogsumlem2  25747  dchrisum0flblem2  25771  dchrisum0fno1  25773  rplogsum  25789  pntrlog2bndlem5  25843  1loopgrvd2  26972  1hevtxdg1  26975  1egrvtxdg1  26978  crctcshwlkn0lem2  27275  crctcshlem4  27284  crctcsh  27288  clwlkclwwlklem2fv1  27459  eulercrct  27707  eucrct2eupth  27710  partfun  30107  ofldchr  30537  psgnfzto1stlem  30660  pmtridfv1  30667  pmtridfv2  30668  smattl  30674  smattr  30675  smatbl  30676  1smat1  30680  madjusmdetlem1  30703  madjusmdetlem2  30704  esumpinfval  30945  eulerpartlemgs2  31251  ballotlemsgt1  31381  ballotlemsel1i  31383  ballotlemsi  31385  signswmnd  31440  signsvtn  31467  cvmliftlem10  32151  unblimceq0lem  33456  poimirlem1  34445  poimirlem2  34446  poimirlem5  34449  poimirlem6  34450  poimirlem12  34456  poimirlem17  34461  poimirlem19  34463  poimirlem20  34464  poimirlem22  34466  poimirlem23  34467  itg2addnc  34498  itg2gt0cn  34499  itgaddnclem2  34503  sdclem1  34571  cdlemefs27cl  37101  flcidc  39280  relexp01min  39564  relexpxpmin  39568  mnurnd  40137  fincygsubgodd  40190  ioondisj2  41330  ioondisj1  41331  lptioo1  41476  limsup10exlem  41616  icccncfext  41733  cncfiooicc  41740  ioodvbdlimc1lem2  41780  ioodvbdlimc2lem  41782  dvnxpaek  41790  ditgeq3d  41812  itgsubsticclem  41823  dirkerper  41945  dirkercncflem2  41953  fourierdlem40  41996  fourierdlem65  42020  fourierdlem74  42029  fourierdlem75  42030  fourierdlem78  42033  fourierdlem81  42036  fourierdlem97  42052  fourierdlem103  42058  fourierdlem104  42059  sqwvfoura  42077  sqwvfourb  42078  fourierswlem  42079  fouriersw  42080  elaa2lem  42082  etransclem19  42102  etransclem22  42105  etransclem24  42107  etransclem35  42118  sge0pnfval  42219  isomenndlem  42376  hoicvrrex  42402  ovn0  42412  volicon0  42421  hsphoidmvle2  42431  hsphoidmvle  42432  hoidmv1lelem1  42437  hoidmv1lelem2  42438  hoidmvlelem2  42442  hoidmvlelem3  42443  hspmbllem1  42472  hspmbllem2  42473  volico2  42487  ovolval2lem  42489  ovnsubadd2lem  42491  ovolval4lem1  42495  vonioolem1  42526  vonioo  42528  vonicclem1  42529  vonicc  42531