Theorem iftrued 4556

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

Syntax hints:   → wi 4   = wceq 1537  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  partfun  6727  mposnif  7566  tz7.44-3  8464  ttrcltr  9785  updjudhcoinlf  10001  iunfictbso  10183  ttukeylem7  10584  max0sub  13258  ifle  13259  xmulneg1  13331  xmulpnf1  13336  expnnval  14115  swrdval2  14694  swrdlend  14701  swrd0  14706  relexp0g  15071  max0add  15359  summolem2a  15763  prodmolem2a  15982  ef0lem  16126  rpnnen2lem3  16264  rpnnen2lem9  16270  iserodd  16882  pcmpt  16939  pcmpt2  16940  prmdvdsprmo  17089  fvprif  17621  setcepi  18155  gsumval2a  18723  smndex2dlinvh  18952  mgm2nsgrplem3  18955  mulgnn  19115  pmtrprfv  19495  pmtrprfval  19529  psgnunilem1  19535  dfod2  19606  oddvds2  19608  cyggenod  19926  fincygsubgodd  20156  mplcoe1  22078  mplcoe5  22081  coe1tm  22297  coe1tmmul2fv  22302  coe1pwmulfv  22304  coe1sclmul  22306  coe1sclmul2  22308  m1detdiag  22624  mdetunilem9  22647  maducoeval2  22667  symgmatr01lem  22680  pmatcollpw3fi1lem1  22813  chpmat1dlem  22862  chfacffsupp  22883  chfacfscmul0  22885  chfacfpmmul0  22889  2ndcdisj  23485  dscmet  24606  xrsxmet  24850  cnmpopc  24974  xrhmeo  24996  oprpiece1res1  25001  htpycc  25031  pcoval1  25065  pcohtpylem  25071  pcoass  25076  pcorevlem  25078  ovolunlem1a  25550  ovolunlem1  25551  ovolicc2lem3  25573  ovolicc2lem4  25574  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  mbfi1fseqlem6  25775  itg2const2  25796  itg2splitlem  25803  itg2split  25804  itg2cnlem1  25816  itg2cnlem2  25817  iblss2  25861  itgspliticc  25892  ditgpos  25911  limcres  25941  plyeq0lem  26269  plypf1  26271  coeeq2  26301  dvply1  26343  aareccl  26386  dvtaylp  26430  pserdvlem2  26490  lgamgulmlem4  27093  isppw  27175  vmappw  27177  muval1  27194  dchrelbasd  27301  dchr1  27319  dchrptlem2  27327  lgsdir2  27392  lgsne0  27397  gausslemma2dlem1a  27427  gausslemma2dlem2  27429  2sqnn0  27500  rplogsumlem2  27547  dchrisum0flblem2  27571  dchrisum0fno1  27573  rplogsum  27589  pntrlog2bndlem5  27643  noinfbnd2  27794  expsnnval  28427  1loopgrvd2  29539  1hevtxdg1  29542  1egrvtxdg1  29545  crctcshwlkn0lem2  29844  crctcshlem4  29853  crctcsh  29857  clwlkclwwlklem2fv1  30027  eulercrct  30274  eucrct2eupth  30277  ccatws1f1o  32918  pmtridfv1  33088  pmtridfv2  33089  psgnfzto1stlem  33093  ofldchr  33309  elrspunsn  33422  gsummoncoe1fzo  33583  rtelextdg2lem  33717  2sqr3minply  33738  smattl  33744  smattr  33745  smatbl  33746  1smat1  33750  madjusmdetlem1  33773  madjusmdetlem2  33774  esumpinfval  34037  eulerpartlemgs2  34345  ballotlemsgt1  34475  ballotlemsel1i  34477  ballotlemsi  34479  signswmnd  34534  signsvtn  34561  cvmliftlem10  35262  unblimceq0lem  36472  bj-rdg0gALT  37037  poimirlem1  37581  poimirlem2  37582  poimirlem5  37585  poimirlem6  37586  poimirlem12  37592  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  poimirlem23  37603  itg2addnc  37634  itg2gt0cn  37635  itgaddnclem2  37639  sdclem1  37703  cdlemefs27cl  40370  sticksstones9  42111  sticksstones10  42112  sticksstones12a  42114  unitscyglem1  42152  metakunt5  42166  metakunt11  42172  metakunt21  42182  metakunt26  42187  metakunt27  42188  metakunt29  42190  metakunt30  42191  metakunt31  42192  flcidc  43131  oe0suclim  43239  tfsconcatfv  43303  safesnsupfilb  43380  relexp01min  43675  relexpxpmin  43679  mnurnd  44252  ioondisj2  45411  ioondisj1  45412  lptioo1  45553  limsup10exlem  45693  icccncfext  45808  cncfiooicc  45815  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnxpaek  45863  ditgeq3d  45885  itgsubsticclem  45896  dirkerper  46017  dirkercncflem2  46025  fourierdlem40  46068  fourierdlem65  46092  fourierdlem74  46101  fourierdlem75  46102  fourierdlem78  46105  fourierdlem81  46108  fourierdlem97  46124  fourierdlem103  46130  fourierdlem104  46131  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  elaa2lem  46154  etransclem19  46174  etransclem22  46177  etransclem24  46179  etransclem35  46190  sge0pnfval  46294  isomenndlem  46451  hoicvrrex  46477  ovn0  46487  volicon0  46496  hsphoidmvle2  46506  hsphoidmvle  46507  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmvlelem2  46517  hoidmvlelem3  46518  hspmbllem1  46547  hspmbllem2  46548  volico2  46562  ovolval2lem  46564  ovnsubadd2lem  46566  ovolval4lem1  46570  vonioolem1  46601  vonioo  46603  vonicclem1  46604  vonicc  46606