Theorem iftrued 4486

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4479

This theorem is referenced by:  partfun  6633  mposnif  7469  tz7.44-3  8337  ttrcltr  9631  updjudhcoinlf  9847  iunfictbso  10027  ttukeylem7  10428  max0sub  13116  ifle  13117  xmulneg1  13189  xmulpnf1  13194  expnnval  13989  swrdval2  14571  swrdlend  14578  swrd0  14583  relexp0g  14947  max0add  15235  summolem2a  15640  prodmolem2a  15859  ef0lem  16003  rpnnen2lem3  16143  rpnnen2lem9  16149  iserodd  16765  pcmpt  16822  pcmpt2  16823  prmdvdsprmo  16972  fvprif  17483  setcepi  18013  gsumval2a  18577  smndex2dlinvh  18809  mgm2nsgrplem3  18812  mulgnn  18972  pmtrprfv  19350  pmtrprfval  19384  psgnunilem1  19390  dfod2  19461  oddvds2  19463  cyggenod  19781  fincygsubgodd  20011  ofldchr  21501  mplcoe1  21960  mplcoe5  21963  coe1tm  22175  coe1tmmul2fv  22180  coe1pwmulfv  22182  coe1sclmul  22184  coe1sclmul2  22186  m1detdiag  22500  mdetunilem9  22523  maducoeval2  22543  symgmatr01lem  22556  pmatcollpw3fi1lem1  22689  chpmat1dlem  22738  chfacffsupp  22759  chfacfscmul0  22761  chfacfpmmul0  22765  2ndcdisj  23359  dscmet  24476  xrsxmet  24714  cnmpopc  24838  xrhmeo  24860  oprpiece1res1  24865  htpycc  24895  pcoval1  24929  pcohtpylem  24935  pcoass  24940  pcorevlem  24942  ovolunlem1a  25413  ovolunlem1  25414  ovolicc2lem3  25436  ovolicc2lem4  25437  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  mbfi1fseqlem6  25637  itg2const2  25658  itg2splitlem  25665  itg2split  25666  itg2cnlem1  25678  itg2cnlem2  25679  iblss2  25723  itgspliticc  25754  ditgpos  25773  limcres  25803  plyeq0lem  26131  plypf1  26133  coeeq2  26163  dvply1  26207  aareccl  26250  dvtaylp  26294  pserdvlem2  26354  lgamgulmlem4  26958  isppw  27040  vmappw  27042  muval1  27059  dchrelbasd  27166  dchr1  27184  dchrptlem2  27192  lgsdir2  27257  lgsne0  27262  gausslemma2dlem1a  27292  gausslemma2dlem2  27294  2sqnn0  27365  rplogsumlem2  27412  dchrisum0flblem2  27436  dchrisum0fno1  27438  rplogsum  27454  pntrlog2bndlem5  27508  noinfbnd2  27659  expsnnval  28336  1loopgrvd2  29467  1hevtxdg1  29470  1egrvtxdg1  29473  crctcshwlkn0lem2  29774  crctcshlem4  29783  crctcsh  29787  clwlkclwwlklem2fv1  29957  eulercrct  30204  eucrct2eupth  30207  ccatws1f1o  32906  pmtridfv1  33050  pmtridfv2  33051  psgnfzto1stlem  33055  elrgspnlem2  33193  elrgspnlem3  33194  elrspunsn  33376  gsummoncoe1fzo  33539  fldextrspunlsp  33645  rtelextdg2lem  33692  2sqr3minply  33746  smattl  33764  smattr  33765  smatbl  33766  1smat1  33770  madjusmdetlem1  33793  madjusmdetlem2  33794  esumpinfval  34039  eulerpartlemgs2  34347  ballotlemsgt1  34478  ballotlemsel1i  34480  ballotlemsi  34482  signswmnd  34524  signsvtn  34551  cvmliftlem10  35266  unblimceq0lem  36479  bj-rdg0gALT  37044  poimirlem1  37600  poimirlem2  37601  poimirlem5  37604  poimirlem6  37605  poimirlem12  37611  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  poimirlem22  37621  poimirlem23  37622  itg2addnc  37653  itg2gt0cn  37654  itgaddnclem2  37658  sdclem1  37722  cdlemefs27cl  40392  sticksstones9  42127  sticksstones10  42128  sticksstones12a  42130  unitscyglem1  42168  flcidc  43143  oe0suclim  43250  tfsconcatfv  43314  safesnsupfilb  43391  relexp01min  43686  relexpxpmin  43690  mnurnd  44256  ioondisj2  45475  ioondisj1  45476  lptioo1  45614  limsup10exlem  45754  icccncfext  45869  cncfiooicc  45876  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  dvnxpaek  45924  ditgeq3d  45946  itgsubsticclem  45957  dirkerper  46078  dirkercncflem2  46086  fourierdlem40  46129  fourierdlem65  46153  fourierdlem74  46162  fourierdlem75  46163  fourierdlem78  46166  fourierdlem81  46169  fourierdlem97  46185  fourierdlem103  46191  fourierdlem104  46192  sqwvfoura  46210  sqwvfourb  46211  fourierswlem  46212  fouriersw  46213  elaa2lem  46215  etransclem19  46235  etransclem22  46238  etransclem24  46240  etransclem35  46251  sge0pnfval  46355  isomenndlem  46512  hoicvrrex  46538  ovn0  46548  volicon0  46557  hsphoidmvle2  46567  hsphoidmvle  46568  hoidmv1lelem1  46573  hoidmv1lelem2  46574  hoidmvlelem2  46578  hoidmvlelem3  46579  hspmbllem1  46608  hspmbllem2  46609  volico2  46623  ovolval2lem  46625  ovnsubadd2lem  46627  ovolval4lem1  46631  vonioolem1  46662  vonioo  46664  vonicclem1  46665  vonicc  46667  discsubc  49050  oppf1st2nd  49117  2oppf  49118  oppfval  49122