Theorem iftrued 4532

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

Syntax hints:   → wi 4   = wceq 1539  ifcif 4524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-if 4525

This theorem is referenced by:  partfun  6714  mposnif  7550  tz7.44-3  8449  ttrcltr  9757  updjudhcoinlf  9973  iunfictbso  10155  ttukeylem7  10556  max0sub  13239  ifle  13240  xmulneg1  13312  xmulpnf1  13317  expnnval  14106  swrdval2  14685  swrdlend  14692  swrd0  14697  relexp0g  15062  max0add  15350  summolem2a  15752  prodmolem2a  15971  ef0lem  16115  rpnnen2lem3  16253  rpnnen2lem9  16259  iserodd  16874  pcmpt  16931  pcmpt2  16932  prmdvdsprmo  17081  fvprif  17607  setcepi  18134  gsumval2a  18699  smndex2dlinvh  18931  mgm2nsgrplem3  18934  mulgnn  19094  pmtrprfv  19472  pmtrprfval  19506  psgnunilem1  19512  dfod2  19583  oddvds2  19585  cyggenod  19903  fincygsubgodd  20133  mplcoe1  22056  mplcoe5  22059  coe1tm  22277  coe1tmmul2fv  22282  coe1pwmulfv  22284  coe1sclmul  22286  coe1sclmul2  22288  m1detdiag  22604  mdetunilem9  22627  maducoeval2  22647  symgmatr01lem  22660  pmatcollpw3fi1lem1  22793  chpmat1dlem  22842  chfacffsupp  22863  chfacfscmul0  22865  chfacfpmmul0  22869  2ndcdisj  23465  dscmet  24586  xrsxmet  24832  cnmpopc  24956  xrhmeo  24978  oprpiece1res1  24983  htpycc  25013  pcoval1  25047  pcohtpylem  25053  pcoass  25058  pcorevlem  25060  ovolunlem1a  25532  ovolunlem1  25533  ovolicc2lem3  25555  ovolicc2lem4  25556  mbfi1fseqlem4  25754  mbfi1fseqlem5  25755  mbfi1fseqlem6  25756  itg2const2  25777  itg2splitlem  25784  itg2split  25785  itg2cnlem1  25797  itg2cnlem2  25798  iblss2  25842  itgspliticc  25873  ditgpos  25892  limcres  25922  plyeq0lem  26250  plypf1  26252  coeeq2  26282  dvply1  26326  aareccl  26369  dvtaylp  26413  pserdvlem2  26473  lgamgulmlem4  27076  isppw  27158  vmappw  27160  muval1  27177  dchrelbasd  27284  dchr1  27302  dchrptlem2  27310  lgsdir2  27375  lgsne0  27380  gausslemma2dlem1a  27410  gausslemma2dlem2  27412  2sqnn0  27483  rplogsumlem2  27530  dchrisum0flblem2  27554  dchrisum0fno1  27556  rplogsum  27572  pntrlog2bndlem5  27626  noinfbnd2  27777  expsnnval  28410  1loopgrvd2  29522  1hevtxdg1  29525  1egrvtxdg1  29528  crctcshwlkn0lem2  29832  crctcshlem4  29841  crctcsh  29845  clwlkclwwlklem2fv1  30015  eulercrct  30262  eucrct2eupth  30265  ccatws1f1o  32937  pmtridfv1  33116  pmtridfv2  33117  psgnfzto1stlem  33121  elrgspnlem2  33248  elrgspnlem3  33249  ofldchr  33345  elrspunsn  33458  gsummoncoe1fzo  33619  fldextrspunlsp  33725  rtelextdg2lem  33768  2sqr3minply  33792  smattl  33798  smattr  33799  smatbl  33800  1smat1  33804  madjusmdetlem1  33827  madjusmdetlem2  33828  esumpinfval  34075  eulerpartlemgs2  34383  ballotlemsgt1  34514  ballotlemsel1i  34516  ballotlemsi  34518  signswmnd  34573  signsvtn  34600  cvmliftlem10  35300  unblimceq0lem  36508  bj-rdg0gALT  37073  poimirlem1  37629  poimirlem2  37630  poimirlem5  37633  poimirlem6  37634  poimirlem12  37640  poimirlem17  37645  poimirlem19  37647  poimirlem20  37648  poimirlem22  37650  poimirlem23  37651  itg2addnc  37682  itg2gt0cn  37683  itgaddnclem2  37687  sdclem1  37751  cdlemefs27cl  40416  sticksstones9  42156  sticksstones10  42157  sticksstones12a  42159  unitscyglem1  42197  metakunt5  42211  metakunt11  42217  metakunt21  42227  metakunt26  42232  metakunt27  42233  metakunt29  42235  metakunt30  42236  metakunt31  42237  flcidc  43187  oe0suclim  43295  tfsconcatfv  43359  safesnsupfilb  43436  relexp01min  43731  relexpxpmin  43735  mnurnd  44307  ioondisj2  45511  ioondisj1  45512  lptioo1  45652  limsup10exlem  45792  icccncfext  45907  cncfiooicc  45914  ioodvbdlimc1lem2  45952  ioodvbdlimc2lem  45954  dvnxpaek  45962  ditgeq3d  45984  itgsubsticclem  45995  dirkerper  46116  dirkercncflem2  46124  fourierdlem40  46167  fourierdlem65  46191  fourierdlem74  46200  fourierdlem75  46201  fourierdlem78  46204  fourierdlem81  46207  fourierdlem97  46223  fourierdlem103  46229  fourierdlem104  46230  sqwvfoura  46248  sqwvfourb  46249  fourierswlem  46250  fouriersw  46251  elaa2lem  46253  etransclem19  46273  etransclem22  46276  etransclem24  46278  etransclem35  46289  sge0pnfval  46393  isomenndlem  46550  hoicvrrex  46576  ovn0  46586  volicon0  46595  hsphoidmvle2  46605  hsphoidmvle  46606  hoidmv1lelem1  46611  hoidmv1lelem2  46612  hoidmvlelem2  46616  hoidmvlelem3  46617  hspmbllem1  46646  hspmbllem2  46647  volico2  46661  ovolval2lem  46663  ovnsubadd2lem  46665  ovolval4lem1  46669  vonioolem1  46700  vonioo  46702  vonicclem1  46703  vonicc  46705