Theorem iftrued 4513

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4505

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-if 4506

This theorem is referenced by:  partfun  6690  mposnif  7528  tz7.44-3  8427  ttrcltr  9735  updjudhcoinlf  9951  iunfictbso  10133  ttukeylem7  10534  max0sub  13217  ifle  13218  xmulneg1  13290  xmulpnf1  13295  expnnval  14087  swrdval2  14669  swrdlend  14676  swrd0  14681  relexp0g  15046  max0add  15334  summolem2a  15736  prodmolem2a  15955  ef0lem  16099  rpnnen2lem3  16239  rpnnen2lem9  16245  iserodd  16860  pcmpt  16917  pcmpt2  16918  prmdvdsprmo  17067  fvprif  17580  setcepi  18106  gsumval2a  18668  smndex2dlinvh  18900  mgm2nsgrplem3  18903  mulgnn  19063  pmtrprfv  19439  pmtrprfval  19473  psgnunilem1  19479  dfod2  19550  oddvds2  19552  cyggenod  19870  fincygsubgodd  20100  mplcoe1  22000  mplcoe5  22003  coe1tm  22215  coe1tmmul2fv  22220  coe1pwmulfv  22222  coe1sclmul  22224  coe1sclmul2  22226  m1detdiag  22540  mdetunilem9  22563  maducoeval2  22583  symgmatr01lem  22596  pmatcollpw3fi1lem1  22729  chpmat1dlem  22778  chfacffsupp  22799  chfacfscmul0  22801  chfacfpmmul0  22805  2ndcdisj  23399  dscmet  24516  xrsxmet  24754  cnmpopc  24878  xrhmeo  24900  oprpiece1res1  24905  htpycc  24935  pcoval1  24969  pcohtpylem  24975  pcoass  24980  pcorevlem  24982  ovolunlem1a  25454  ovolunlem1  25455  ovolicc2lem3  25477  ovolicc2lem4  25478  mbfi1fseqlem4  25676  mbfi1fseqlem5  25677  mbfi1fseqlem6  25678  itg2const2  25699  itg2splitlem  25706  itg2split  25707  itg2cnlem1  25719  itg2cnlem2  25720  iblss2  25764  itgspliticc  25795  ditgpos  25814  limcres  25844  plyeq0lem  26172  plypf1  26174  coeeq2  26204  dvply1  26248  aareccl  26291  dvtaylp  26335  pserdvlem2  26395  lgamgulmlem4  26999  isppw  27081  vmappw  27083  muval1  27100  dchrelbasd  27207  dchr1  27225  dchrptlem2  27233  lgsdir2  27298  lgsne0  27303  gausslemma2dlem1a  27333  gausslemma2dlem2  27335  2sqnn0  27406  rplogsumlem2  27453  dchrisum0flblem2  27477  dchrisum0fno1  27479  rplogsum  27495  pntrlog2bndlem5  27549  noinfbnd2  27700  expsnnval  28369  1loopgrvd2  29488  1hevtxdg1  29491  1egrvtxdg1  29494  crctcshwlkn0lem2  29798  crctcshlem4  29807  crctcsh  29811  clwlkclwwlklem2fv1  29981  eulercrct  30228  eucrct2eupth  30231  ccatws1f1o  32932  pmtridfv1  33111  pmtridfv2  33112  psgnfzto1stlem  33116  elrgspnlem2  33243  elrgspnlem3  33244  ofldchr  33341  elrspunsn  33449  gsummoncoe1fzo  33612  fldextrspunlsp  33720  rtelextdg2lem  33765  2sqr3minply  33819  smattl  33834  smattr  33835  smatbl  33836  1smat1  33840  madjusmdetlem1  33863  madjusmdetlem2  33864  esumpinfval  34109  eulerpartlemgs2  34417  ballotlemsgt1  34548  ballotlemsel1i  34550  ballotlemsi  34552  signswmnd  34594  signsvtn  34621  cvmliftlem10  35321  unblimceq0lem  36529  bj-rdg0gALT  37094  poimirlem1  37650  poimirlem2  37651  poimirlem5  37654  poimirlem6  37655  poimirlem12  37661  poimirlem17  37666  poimirlem19  37668  poimirlem20  37669  poimirlem22  37671  poimirlem23  37672  itg2addnc  37703  itg2gt0cn  37704  itgaddnclem2  37708  sdclem1  37772  cdlemefs27cl  40437  sticksstones9  42172  sticksstones10  42173  sticksstones12a  42175  unitscyglem1  42213  flcidc  43169  oe0suclim  43276  tfsconcatfv  43340  safesnsupfilb  43417  relexp01min  43712  relexpxpmin  43716  mnurnd  44282  ioondisj2  45502  ioondisj1  45503  lptioo1  45641  limsup10exlem  45781  icccncfext  45896  cncfiooicc  45903  ioodvbdlimc1lem2  45941  ioodvbdlimc2lem  45943  dvnxpaek  45951  ditgeq3d  45973  itgsubsticclem  45984  dirkerper  46105  dirkercncflem2  46113  fourierdlem40  46156  fourierdlem65  46180  fourierdlem74  46189  fourierdlem75  46190  fourierdlem78  46193  fourierdlem81  46196  fourierdlem97  46212  fourierdlem103  46218  fourierdlem104  46219  sqwvfoura  46237  sqwvfourb  46238  fourierswlem  46239  fouriersw  46240  elaa2lem  46242  etransclem19  46262  etransclem22  46265  etransclem24  46267  etransclem35  46278  sge0pnfval  46382  isomenndlem  46539  hoicvrrex  46565  ovn0  46575  volicon0  46584  hsphoidmvle2  46594  hsphoidmvle  46595  hoidmv1lelem1  46600  hoidmv1lelem2  46601  hoidmvlelem2  46605  hoidmvlelem3  46606  hspmbllem1  46635  hspmbllem2  46636  volico2  46650  ovolval2lem  46652  ovnsubadd2lem  46654  ovolval4lem1  46658  vonioolem1  46689  vonioo  46691  vonicclem1  46692  vonicc  46694  discsubc  49011  oppf1st2nd  49059  2oppf  49060  oppfval  49062