MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iftrued Structured version   Visualization version   GIF version

Theorem iftrued 4473
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
StepHypRef Expression
1 iftrued.1 . 2 (𝜑𝜒)
2 iftrue 4471 . 2 (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
31, 2syl 17 1 (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  ifcif 4465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-ex 1772  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4466
This theorem is referenced by:  mposnif  7257  tz7.44-3  8035  updjudhcoinlf  9350  iunfictbso  9529  ttukeylem7  9926  max0sub  12579  ifle  12580  xmulneg1  12652  xmulpnf1  12657  expnnval  13422  swrdval2  13998  swrdlend  14005  swrd0  14010  relexp0g  14371  max0add  14660  summolem2a  15062  prodmolem2a  15278  ef0lem  15422  rpnnen2lem3  15559  rpnnen2lem9  15565  iserodd  16162  pcmpt  16218  pcmpt2  16219  prmdvdsprmo  16368  fvprif  16824  setcepi  17338  gsumval2a  17885  mgm2nsgrplem3  18025  mulgnn  18172  pmtrprfv  18512  pmtrprfval  18546  psgnunilem1  18552  dfod2  18622  oddvds2  18624  cyggenod  18934  fincygsubgodd  19165  mplcoe1  20176  mplcoe5  20179  coe1tm  20371  coe1tmmul2fv  20376  coe1pwmulfv  20378  coe1sclmul  20380  coe1sclmul2  20382  m1detdiag  21136  mdetunilem9  21159  maducoeval2  21179  symgmatr01lem  21192  pmatcollpw3fi1lem1  21324  chpmat1dlem  21373  chfacffsupp  21394  chfacfscmul0  21396  chfacfpmmul0  21400  2ndcdisj  21994  dscmet  23111  xrsxmet  23346  cnmpopc  23461  xrhmeo  23479  oprpiece1res1  23484  htpycc  23513  pcoval1  23546  pcohtpylem  23552  pcoass  23557  pcorevlem  23559  ovolunlem1a  24026  ovolunlem1  24027  ovolicc2lem3  24049  ovolicc2lem4  24050  mbfi1fseqlem4  24248  mbfi1fseqlem5  24249  mbfi1fseqlem6  24250  itg2const2  24271  itg2splitlem  24278  itg2split  24279  itg2cnlem1  24291  itg2cnlem2  24292  iblss2  24335  itgspliticc  24366  ditgpos  24383  limcres  24413  plyeq0lem  24729  plypf1  24731  coeeq2  24761  dvply1  24802  aareccl  24844  dvtaylp  24887  pserdvlem2  24945  lgamgulmlem4  25537  isppw  25619  vmappw  25621  muval1  25638  dchrelbasd  25743  dchr1  25761  dchrptlem2  25769  lgsdir2  25834  lgsne0  25839  gausslemma2dlem1a  25869  gausslemma2dlem2  25871  2sqnn0  25942  rplogsumlem2  25989  dchrisum0flblem2  26013  dchrisum0fno1  26015  rplogsum  26031  pntrlog2bndlem5  26085  1loopgrvd2  27213  1hevtxdg1  27216  1egrvtxdg1  27219  crctcshwlkn0lem2  27517  crctcshlem4  27526  crctcsh  27530  clwlkclwwlklem2fv1  27701  eulercrct  27949  eucrct2eupth  27952  partfun  30350  pmtridfv1  30665  pmtridfv2  30666  psgnfzto1stlem  30670  ofldchr  30815  smattl  30963  smattr  30964  smatbl  30965  1smat1  30969  madjusmdetlem1  30992  madjusmdetlem2  30993  esumpinfval  31232  eulerpartlemgs2  31538  ballotlemsgt1  31668  ballotlemsel1i  31670  ballotlemsi  31672  signswmnd  31727  signsvtn  31754  cvmliftlem10  32439  unblimceq0lem  33743  poimirlem1  34775  poimirlem2  34776  poimirlem5  34779  poimirlem6  34780  poimirlem12  34786  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem22  34796  poimirlem23  34797  itg2addnc  34828  itg2gt0cn  34829  itgaddnclem2  34833  sdclem1  34901  cdlemefs27cl  37431  flcidc  39654  relexp01min  39938  relexpxpmin  39942  mnurnd  40499  ioondisj2  41647  ioondisj1  41648  lptioo1  41793  limsup10exlem  41933  icccncfext  42050  cncfiooicc  42057  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvnxpaek  42107  ditgeq3d  42129  itgsubsticclem  42140  dirkerper  42262  dirkercncflem2  42270  fourierdlem40  42313  fourierdlem65  42337  fourierdlem74  42346  fourierdlem75  42347  fourierdlem78  42350  fourierdlem81  42353  fourierdlem97  42369  fourierdlem103  42375  fourierdlem104  42376  sqwvfoura  42394  sqwvfourb  42395  fourierswlem  42396  fouriersw  42397  elaa2lem  42399  etransclem19  42419  etransclem22  42422  etransclem24  42424  etransclem35  42435  sge0pnfval  42536  isomenndlem  42693  hoicvrrex  42719  ovn0  42729  volicon0  42738  hsphoidmvle2  42748  hsphoidmvle  42749  hoidmv1lelem1  42754  hoidmv1lelem2  42755  hoidmvlelem2  42759  hoidmvlelem3  42760  hspmbllem1  42789  hspmbllem2  42790  volico2  42804  ovolval2lem  42806  ovnsubadd2lem  42808  ovolval4lem1  42812  vonioolem1  42843  vonioo  42845  vonicclem1  42846  vonicc  42848  smndex2dlinvh  43987
  Copyright terms: Public domain W3C validator