Theorem iftrued 4468

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

Syntax hints:   → wi 4   = wceq 1539  ifcif 4460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-if 4461

This theorem is referenced by:  partfun  6589  mposnif  7399  tz7.44-3  8248  ttrcltr  9483  updjudhcoinlf  9699  iunfictbso  9879  ttukeylem7  10280  max0sub  12939  ifle  12940  xmulneg1  13012  xmulpnf1  13017  expnnval  13794  swrdval2  14368  swrdlend  14375  swrd0  14380  relexp0g  14742  max0add  15031  summolem2a  15436  prodmolem2a  15653  ef0lem  15797  rpnnen2lem3  15934  rpnnen2lem9  15940  iserodd  16545  pcmpt  16602  pcmpt2  16603  prmdvdsprmo  16752  fvprif  17281  setcepi  17812  gsumval2a  18378  smndex2dlinvh  18565  mgm2nsgrplem3  18568  mulgnn  18717  pmtrprfv  19070  pmtrprfval  19104  psgnunilem1  19110  dfod2  19180  oddvds2  19182  cyggenod  19493  fincygsubgodd  19724  mplcoe1  21247  mplcoe5  21250  coe1tm  21453  coe1tmmul2fv  21458  coe1pwmulfv  21460  coe1sclmul  21462  coe1sclmul2  21464  m1detdiag  21755  mdetunilem9  21778  maducoeval2  21798  symgmatr01lem  21811  pmatcollpw3fi1lem1  21944  chpmat1dlem  21993  chfacffsupp  22014  chfacfscmul0  22016  chfacfpmmul0  22020  2ndcdisj  22616  dscmet  23737  xrsxmet  23981  cnmpopc  24100  xrhmeo  24118  oprpiece1res1  24123  htpycc  24152  pcoval1  24185  pcohtpylem  24191  pcoass  24196  pcorevlem  24198  ovolunlem1a  24669  ovolunlem1  24670  ovolicc2lem3  24692  ovolicc2lem4  24693  mbfi1fseqlem4  24892  mbfi1fseqlem5  24893  mbfi1fseqlem6  24894  itg2const2  24915  itg2splitlem  24922  itg2split  24923  itg2cnlem1  24935  itg2cnlem2  24936  iblss2  24979  itgspliticc  25010  ditgpos  25029  limcres  25059  plyeq0lem  25380  plypf1  25382  coeeq2  25412  dvply1  25453  aareccl  25495  dvtaylp  25538  pserdvlem2  25596  lgamgulmlem4  26190  isppw  26272  vmappw  26274  muval1  26291  dchrelbasd  26396  dchr1  26414  dchrptlem2  26422  lgsdir2  26487  lgsne0  26492  gausslemma2dlem1a  26522  gausslemma2dlem2  26524  2sqnn0  26595  rplogsumlem2  26642  dchrisum0flblem2  26666  dchrisum0fno1  26668  rplogsum  26684  pntrlog2bndlem5  26738  1loopgrvd2  27879  1hevtxdg1  27882  1egrvtxdg1  27885  crctcshwlkn0lem2  28185  crctcshlem4  28194  crctcsh  28198  clwlkclwwlklem2fv1  28368  eulercrct  28615  eucrct2eupth  28618  pmtridfv1  31371  pmtridfv2  31372  psgnfzto1stlem  31376  ofldchr  31522  smattl  31757  smattr  31758  smatbl  31759  1smat1  31763  madjusmdetlem1  31786  madjusmdetlem2  31787  esumpinfval  32050  eulerpartlemgs2  32356  ballotlemsgt1  32486  ballotlemsel1i  32488  ballotlemsi  32490  signswmnd  32545  signsvtn  32572  cvmliftlem10  33265  noinfbnd2  33943  unblimceq0lem  34695  bj-rdg0gALT  35251  poimirlem1  35787  poimirlem2  35788  poimirlem5  35791  poimirlem6  35792  poimirlem12  35798  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem22  35808  poimirlem23  35809  itg2addnc  35840  itg2gt0cn  35841  itgaddnclem2  35845  sdclem1  35910  cdlemefs27cl  38434  sticksstones9  40117  sticksstones10  40118  sticksstones12a  40120  metakunt5  40136  metakunt11  40142  metakunt21  40152  metakunt26  40157  metakunt27  40158  metakunt29  40160  metakunt30  40161  metakunt31  40162  flcidc  41006  relexp01min  41328  relexpxpmin  41332  mnurnd  41908  ioondisj2  43038  ioondisj1  43039  lptioo1  43180  limsup10exlem  43320  icccncfext  43435  cncfiooicc  43442  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnxpaek  43490  ditgeq3d  43512  itgsubsticclem  43523  dirkerper  43644  dirkercncflem2  43652  fourierdlem40  43695  fourierdlem65  43719  fourierdlem74  43728  fourierdlem75  43729  fourierdlem78  43732  fourierdlem81  43735  fourierdlem97  43751  fourierdlem103  43757  fourierdlem104  43758  sqwvfoura  43776  sqwvfourb  43777  fourierswlem  43778  fouriersw  43779  elaa2lem  43781  etransclem19  43801  etransclem22  43804  etransclem24  43806  etransclem35  43817  sge0pnfval  43918  isomenndlem  44075  hoicvrrex  44101  ovn0  44111  volicon0  44120  hsphoidmvle2  44130  hsphoidmvle  44131  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmvlelem2  44141  hoidmvlelem3  44142  hspmbllem1  44171  hspmbllem2  44172  volico2  44186  ovolval2lem  44188  ovnsubadd2lem  44190  ovolval4lem1  44194  vonioolem1  44225  vonioo  44227  vonicclem1  44228  vonicc  44230