Theorem iftrued 4464

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

Syntax hints:   → wi 4   = wceq 1539  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-if 4457

This theorem is referenced by:  partfun  6564  mposnif  7368  tz7.44-3  8210  updjudhcoinlf  9621  iunfictbso  9801  ttukeylem7  10202  max0sub  12859  ifle  12860  xmulneg1  12932  xmulpnf1  12937  expnnval  13713  swrdval2  14287  swrdlend  14294  swrd0  14299  relexp0g  14661  max0add  14950  summolem2a  15355  prodmolem2a  15572  ef0lem  15716  rpnnen2lem3  15853  rpnnen2lem9  15859  iserodd  16464  pcmpt  16521  pcmpt2  16522  prmdvdsprmo  16671  fvprif  17189  setcepi  17719  gsumval2a  18284  smndex2dlinvh  18471  mgm2nsgrplem3  18474  mulgnn  18623  pmtrprfv  18976  pmtrprfval  19010  psgnunilem1  19016  dfod2  19086  oddvds2  19088  cyggenod  19399  fincygsubgodd  19630  mplcoe1  21148  mplcoe5  21151  coe1tm  21354  coe1tmmul2fv  21359  coe1pwmulfv  21361  coe1sclmul  21363  coe1sclmul2  21365  m1detdiag  21654  mdetunilem9  21677  maducoeval2  21697  symgmatr01lem  21710  pmatcollpw3fi1lem1  21843  chpmat1dlem  21892  chfacffsupp  21913  chfacfscmul0  21915  chfacfpmmul0  21919  2ndcdisj  22515  dscmet  23634  xrsxmet  23878  cnmpopc  23997  xrhmeo  24015  oprpiece1res1  24020  htpycc  24049  pcoval1  24082  pcohtpylem  24088  pcoass  24093  pcorevlem  24095  ovolunlem1a  24565  ovolunlem1  24566  ovolicc2lem3  24588  ovolicc2lem4  24589  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  mbfi1fseqlem6  24790  itg2const2  24811  itg2splitlem  24818  itg2split  24819  itg2cnlem1  24831  itg2cnlem2  24832  iblss2  24875  itgspliticc  24906  ditgpos  24925  limcres  24955  plyeq0lem  25276  plypf1  25278  coeeq2  25308  dvply1  25349  aareccl  25391  dvtaylp  25434  pserdvlem2  25492  lgamgulmlem4  26086  isppw  26168  vmappw  26170  muval1  26187  dchrelbasd  26292  dchr1  26310  dchrptlem2  26318  lgsdir2  26383  lgsne0  26388  gausslemma2dlem1a  26418  gausslemma2dlem2  26420  2sqnn0  26491  rplogsumlem2  26538  dchrisum0flblem2  26562  dchrisum0fno1  26564  rplogsum  26580  pntrlog2bndlem5  26634  1loopgrvd2  27773  1hevtxdg1  27776  1egrvtxdg1  27779  crctcshwlkn0lem2  28077  crctcshlem4  28086  crctcsh  28090  clwlkclwwlklem2fv1  28260  eulercrct  28507  eucrct2eupth  28510  pmtridfv1  31264  pmtridfv2  31265  psgnfzto1stlem  31269  ofldchr  31415  smattl  31650  smattr  31651  smatbl  31652  1smat1  31656  madjusmdetlem1  31679  madjusmdetlem2  31680  esumpinfval  31941  eulerpartlemgs2  32247  ballotlemsgt1  32377  ballotlemsel1i  32379  ballotlemsi  32381  signswmnd  32436  signsvtn  32463  cvmliftlem10  33156  ttrcltr  33702  noinfbnd2  33861  unblimceq0lem  34613  bj-rdg0gALT  35169  poimirlem1  35705  poimirlem2  35706  poimirlem5  35709  poimirlem6  35710  poimirlem12  35716  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem22  35726  poimirlem23  35727  itg2addnc  35758  itg2gt0cn  35759  itgaddnclem2  35763  sdclem1  35828  cdlemefs27cl  38354  sticksstones9  40038  sticksstones10  40039  sticksstones12a  40041  metakunt5  40057  metakunt11  40063  metakunt21  40073  metakunt26  40078  metakunt27  40079  metakunt29  40081  metakunt30  40082  metakunt31  40083  flcidc  40915  relexp01min  41210  relexpxpmin  41214  mnurnd  41790  ioondisj2  42921  ioondisj1  42922  lptioo1  43063  limsup10exlem  43203  icccncfext  43318  cncfiooicc  43325  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnxpaek  43373  ditgeq3d  43395  itgsubsticclem  43406  dirkerper  43527  dirkercncflem2  43535  fourierdlem40  43578  fourierdlem65  43602  fourierdlem74  43611  fourierdlem75  43612  fourierdlem78  43615  fourierdlem81  43618  fourierdlem97  43634  fourierdlem103  43640  fourierdlem104  43641  sqwvfoura  43659  sqwvfourb  43660  fourierswlem  43661  fouriersw  43662  elaa2lem  43664  etransclem19  43684  etransclem22  43687  etransclem24  43689  etransclem35  43700  sge0pnfval  43801  isomenndlem  43958  hoicvrrex  43984  ovn0  43994  volicon0  44003  hsphoidmvle2  44013  hsphoidmvle  44014  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmvlelem2  44024  hoidmvlelem3  44025  hspmbllem1  44054  hspmbllem2  44055  volico2  44069  ovolval2lem  44071  ovnsubadd2lem  44073  ovolval4lem1  44077  vonioolem1  44108  vonioo  44110  vonicclem1  44111  vonicc  44113