Theorem iftrued 4473

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

Syntax hints:   → wi 4   = wceq 1542  ifcif 4465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-if 4466

This theorem is referenced by:  partfun  6578  mposnif  7384  tz7.44-3  8230  ttrcltr  9452  updjudhcoinlf  9691  iunfictbso  9871  ttukeylem7  10272  max0sub  12929  ifle  12930  xmulneg1  13002  xmulpnf1  13007  expnnval  13783  swrdval2  14357  swrdlend  14364  swrd0  14369  relexp0g  14731  max0add  15020  summolem2a  15425  prodmolem2a  15642  ef0lem  15786  rpnnen2lem3  15923  rpnnen2lem9  15929  iserodd  16534  pcmpt  16591  pcmpt2  16592  prmdvdsprmo  16741  fvprif  17270  setcepi  17801  gsumval2a  18367  smndex2dlinvh  18554  mgm2nsgrplem3  18557  mulgnn  18706  pmtrprfv  19059  pmtrprfval  19093  psgnunilem1  19099  dfod2  19169  oddvds2  19171  cyggenod  19482  fincygsubgodd  19713  mplcoe1  21236  mplcoe5  21239  coe1tm  21442  coe1tmmul2fv  21447  coe1pwmulfv  21449  coe1sclmul  21451  coe1sclmul2  21453  m1detdiag  21744  mdetunilem9  21767  maducoeval2  21787  symgmatr01lem  21800  pmatcollpw3fi1lem1  21933  chpmat1dlem  21982  chfacffsupp  22003  chfacfscmul0  22005  chfacfpmmul0  22009  2ndcdisj  22605  dscmet  23726  xrsxmet  23970  cnmpopc  24089  xrhmeo  24107  oprpiece1res1  24112  htpycc  24141  pcoval1  24174  pcohtpylem  24180  pcoass  24185  pcorevlem  24187  ovolunlem1a  24658  ovolunlem1  24659  ovolicc2lem3  24681  ovolicc2lem4  24682  mbfi1fseqlem4  24881  mbfi1fseqlem5  24882  mbfi1fseqlem6  24883  itg2const2  24904  itg2splitlem  24911  itg2split  24912  itg2cnlem1  24924  itg2cnlem2  24925  iblss2  24968  itgspliticc  24999  ditgpos  25018  limcres  25048  plyeq0lem  25369  plypf1  25371  coeeq2  25401  dvply1  25442  aareccl  25484  dvtaylp  25527  pserdvlem2  25585  lgamgulmlem4  26179  isppw  26261  vmappw  26263  muval1  26280  dchrelbasd  26385  dchr1  26403  dchrptlem2  26411  lgsdir2  26476  lgsne0  26481  gausslemma2dlem1a  26511  gausslemma2dlem2  26513  2sqnn0  26584  rplogsumlem2  26631  dchrisum0flblem2  26655  dchrisum0fno1  26657  rplogsum  26673  pntrlog2bndlem5  26727  1loopgrvd2  27868  1hevtxdg1  27871  1egrvtxdg1  27874  crctcshwlkn0lem2  28172  crctcshlem4  28181  crctcsh  28185  clwlkclwwlklem2fv1  28355  eulercrct  28602  eucrct2eupth  28605  pmtridfv1  31358  pmtridfv2  31359  psgnfzto1stlem  31363  ofldchr  31509  smattl  31744  smattr  31745  smatbl  31746  1smat1  31750  madjusmdetlem1  31773  madjusmdetlem2  31774  esumpinfval  32037  eulerpartlemgs2  32343  ballotlemsgt1  32473  ballotlemsel1i  32475  ballotlemsi  32477  signswmnd  32532  signsvtn  32559  cvmliftlem10  33252  noinfbnd2  33930  unblimceq0lem  34682  bj-rdg0gALT  35238  poimirlem1  35774  poimirlem2  35775  poimirlem5  35778  poimirlem6  35779  poimirlem12  35785  poimirlem17  35790  poimirlem19  35792  poimirlem20  35793  poimirlem22  35795  poimirlem23  35796  itg2addnc  35827  itg2gt0cn  35828  itgaddnclem2  35832  sdclem1  35897  cdlemefs27cl  38423  sticksstones9  40107  sticksstones10  40108  sticksstones12a  40110  metakunt5  40126  metakunt11  40132  metakunt21  40142  metakunt26  40147  metakunt27  40148  metakunt29  40150  metakunt30  40151  metakunt31  40152  flcidc  40996  relexp01min  41291  relexpxpmin  41295  mnurnd  41871  ioondisj2  43002  ioondisj1  43003  lptioo1  43144  limsup10exlem  43284  icccncfext  43399  cncfiooicc  43406  ioodvbdlimc1lem2  43444  ioodvbdlimc2lem  43446  dvnxpaek  43454  ditgeq3d  43476  itgsubsticclem  43487  dirkerper  43608  dirkercncflem2  43616  fourierdlem40  43659  fourierdlem65  43683  fourierdlem74  43692  fourierdlem75  43693  fourierdlem78  43696  fourierdlem81  43699  fourierdlem97  43715  fourierdlem103  43721  fourierdlem104  43722  sqwvfoura  43740  sqwvfourb  43741  fourierswlem  43742  fouriersw  43743  elaa2lem  43745  etransclem19  43765  etransclem22  43768  etransclem24  43770  etransclem35  43781  sge0pnfval  43882  isomenndlem  44039  hoicvrrex  44065  ovn0  44075  volicon0  44084  hsphoidmvle2  44094  hsphoidmvle  44095  hoidmv1lelem1  44100  hoidmv1lelem2  44101  hoidmvlelem2  44105  hoidmvlelem3  44106  hspmbllem1  44135  hspmbllem2  44136  volico2  44150  ovolval2lem  44152  ovnsubadd2lem  44154  ovolval4lem1  44158  vonioolem1  44189  vonioo  44191  vonicclem1  44192  vonicc  44194