Theorem iftrued 4537

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

Syntax hints:   → wi 4   = wceq 1542  ifcif 4529

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  partfun  6698  mposnif  7524  tz7.44-3  8408  ttrcltr  9711  updjudhcoinlf  9927  iunfictbso  10109  ttukeylem7  10510  max0sub  13175  ifle  13176  xmulneg1  13248  xmulpnf1  13253  expnnval  14030  swrdval2  14596  swrdlend  14603  swrd0  14608  relexp0g  14969  max0add  15257  summolem2a  15661  prodmolem2a  15878  ef0lem  16022  rpnnen2lem3  16159  rpnnen2lem9  16165  iserodd  16768  pcmpt  16825  pcmpt2  16826  prmdvdsprmo  16975  fvprif  17507  setcepi  18038  gsumval2a  18604  smndex2dlinvh  18798  mgm2nsgrplem3  18801  mulgnn  18958  pmtrprfv  19321  pmtrprfval  19355  psgnunilem1  19361  dfod2  19432  oddvds2  19434  cyggenod  19752  fincygsubgodd  19982  mplcoe1  21592  mplcoe5  21595  coe1tm  21795  coe1tmmul2fv  21800  coe1pwmulfv  21802  coe1sclmul  21804  coe1sclmul2  21806  m1detdiag  22099  mdetunilem9  22122  maducoeval2  22142  symgmatr01lem  22155  pmatcollpw3fi1lem1  22288  chpmat1dlem  22337  chfacffsupp  22358  chfacfscmul0  22360  chfacfpmmul0  22364  2ndcdisj  22960  dscmet  24081  xrsxmet  24325  cnmpopc  24444  xrhmeo  24462  oprpiece1res1  24467  htpycc  24496  pcoval1  24529  pcohtpylem  24535  pcoass  24540  pcorevlem  24542  ovolunlem1a  25013  ovolunlem1  25014  ovolicc2lem3  25036  ovolicc2lem4  25037  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  mbfi1fseqlem6  25238  itg2const2  25259  itg2splitlem  25266  itg2split  25267  itg2cnlem1  25279  itg2cnlem2  25280  iblss2  25323  itgspliticc  25354  ditgpos  25373  limcres  25403  plyeq0lem  25724  plypf1  25726  coeeq2  25756  dvply1  25797  aareccl  25839  dvtaylp  25882  pserdvlem2  25940  lgamgulmlem4  26536  isppw  26618  vmappw  26620  muval1  26637  dchrelbasd  26742  dchr1  26760  dchrptlem2  26768  lgsdir2  26833  lgsne0  26838  gausslemma2dlem1a  26868  gausslemma2dlem2  26870  2sqnn0  26941  rplogsumlem2  26988  dchrisum0flblem2  27012  dchrisum0fno1  27014  rplogsum  27030  pntrlog2bndlem5  27084  noinfbnd2  27234  1loopgrvd2  28760  1hevtxdg1  28763  1egrvtxdg1  28766  crctcshwlkn0lem2  29065  crctcshlem4  29074  crctcsh  29078  clwlkclwwlklem2fv1  29248  eulercrct  29495  eucrct2eupth  29498  pmtridfv1  32254  pmtridfv2  32255  psgnfzto1stlem  32259  ofldchr  32432  elrspunsn  32547  gsummoncoe1fzo  32668  smattl  32778  smattr  32779  smatbl  32780  1smat1  32784  madjusmdetlem1  32807  madjusmdetlem2  32808  esumpinfval  33071  eulerpartlemgs2  33379  ballotlemsgt1  33509  ballotlemsel1i  33511  ballotlemsi  33513  signswmnd  33568  signsvtn  33595  cvmliftlem10  34285  unblimceq0lem  35382  bj-rdg0gALT  35952  poimirlem1  36489  poimirlem2  36490  poimirlem5  36493  poimirlem6  36494  poimirlem12  36500  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem22  36510  poimirlem23  36511  itg2addnc  36542  itg2gt0cn  36543  itgaddnclem2  36547  sdclem1  36611  cdlemefs27cl  39284  sticksstones9  40970  sticksstones10  40971  sticksstones12a  40973  metakunt5  40989  metakunt11  40995  metakunt21  41005  metakunt26  41010  metakunt27  41011  metakunt29  41013  metakunt30  41014  metakunt31  41015  flcidc  41916  oe0suclim  42027  tfsconcatfv  42091  safesnsupfilb  42169  relexp01min  42464  relexpxpmin  42468  mnurnd  43042  ioondisj2  44206  ioondisj1  44207  lptioo1  44348  limsup10exlem  44488  icccncfext  44603  cncfiooicc  44610  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnxpaek  44658  ditgeq3d  44680  itgsubsticclem  44691  dirkerper  44812  dirkercncflem2  44820  fourierdlem40  44863  fourierdlem65  44887  fourierdlem74  44896  fourierdlem75  44897  fourierdlem78  44900  fourierdlem81  44903  fourierdlem97  44919  fourierdlem103  44925  fourierdlem104  44926  sqwvfoura  44944  sqwvfourb  44945  fourierswlem  44946  fouriersw  44947  elaa2lem  44949  etransclem19  44969  etransclem22  44972  etransclem24  44974  etransclem35  44985  sge0pnfval  45089  isomenndlem  45246  hoicvrrex  45272  ovn0  45282  volicon0  45291  hsphoidmvle2  45301  hsphoidmvle  45302  hoidmv1lelem1  45307  hoidmv1lelem2  45308  hoidmvlelem2  45312  hoidmvlelem3  45313  hspmbllem1  45342  hspmbllem2  45343  volico2  45357  ovolval2lem  45359  ovnsubadd2lem  45361  ovolval4lem1  45365  vonioolem1  45396  vonioo  45398  vonicclem1  45399  vonicc  45401