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

Theorem iftrued 4044
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 4042 . 2 (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
31, 2syl 17 1 (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  ifcif 4036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037
This theorem is referenced by:  mpt2snif  6652  tz7.44-3  7391  iunfictbso  8820  ttukeylem7  9220  max0sub  11901  ifle  11902  xmulneg1  11971  xmulpnf1  11976  expnnval  12725  swrdval2  13272  swrdlend  13283  swrd0  13286  swrdccatid  13348  relexp0g  13610  max0add  13898  summolem2a  14293  prodmolem2a  14503  ef0lem  14648  rpnnen2lem3  14784  rpnnen2lem9  14790  iserodd  15378  pcmpt  15434  pcmpt2  15435  prmdvdsprmo  15584  setcepi  16561  gsumval2a  17102  mgm2nsgrplem3  17230  mulgnn  17370  pmtrprfv  17696  pmtrprfval  17730  psgnunilem1  17736  dfod2  17804  oddvds2  17806  cyggenod  18109  mplcoe1  19286  mplcoe5  19289  coe1tm  19464  coe1tmmul2fv  19469  coe1pwmulfv  19471  coe1sclmul  19473  coe1sclmul2  19475  m1detdiag  20222  mdetunilem9  20245  maducoeval2  20265  symgmatr01lem  20278  pmatcollpw3fi1lem1  20410  chpmat1dlem  20459  chfacffsupp  20480  chfacfscmul0  20482  chfacfpmmul0  20486  2ndcdisj  21069  dscmet  22187  xrsxmet  22420  cnmpt2pc  22535  xrhmeo  22553  oprpiece1res1  22558  htpycc  22587  pcoval1  22621  pcohtpylem  22627  pcoass  22632  pcorevlem  22634  ovolunlem1a  23071  ovolunlem1  23072  ovolicc2lem3  23094  ovolicc2lem4  23095  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mbfi1fseqlem6  23293  itg2const2  23314  itg2splitlem  23321  itg2split  23322  itg2cnlem1  23334  itg2cnlem2  23335  iblss2  23378  itgspliticc  23409  ditgpos  23426  limcres  23456  plyeq0lem  23770  plypf1  23772  coeeq2  23802  dvply1  23843  aareccl  23885  dvtaylp  23928  pserdvlem2  23986  lgamgulmlem4  24558  isppw  24640  vmappw  24642  muval1  24659  dchrelbasd  24764  dchr1  24782  dchrptlem2  24790  lgsdir2  24855  lgsne0  24860  gausslemma2dlem1a  24890  gausslemma2dlem2  24892  rplogsumlem2  24974  dchrisum0flblem2  24998  dchrisum0fno1  25000  rplogsum  25016  pntrlog2bndlem5  25070  clwlkisclwwlklem2fv1  26310  eupath2  26507  partfun  28858  ofldchr  29145  psgnfzto1stlem  29181  smattl  29192  smattr  29193  smatbl  29194  1smat1  29198  madjusmdetlem1  29221  madjusmdetlem2  29222  esumpinfval  29462  eulerpartlemgs2  29769  ballotlemsgt1  29899  ballotlemsel1i  29901  ballotlemsi  29903  signswmnd  29960  signsvtn  29987  cvmliftlem10  30530  unblimceq0lem  31667  poimirlem1  32580  poimirlem2  32581  poimirlem5  32584  poimirlem6  32585  poimirlem12  32591  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem22  32601  poimirlem23  32602  itg2addnc  32634  itg2gt0cn  32635  itgaddnclem2  32639  sdclem1  32709  cdlemefs27cl  34719  flcidc  36763  relexp01min  37024  relexpxpmin  37028  ioondisj2  38561  ioondisj1  38562  lptioo1  38699  icccncfext  38773  cncfiooicc  38780  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnxpaek  38832  ditgeq3d  38856  itgsubsticclem  38867  dirkerper  38989  dirkercncflem2  38997  fourierdlem40  39040  fourierdlem65  39064  fourierdlem74  39073  fourierdlem75  39074  fourierdlem78  39077  fourierdlem81  39080  fourierdlem97  39096  fourierdlem103  39102  fourierdlem104  39103  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  elaa2lem  39126  etransclem19  39146  etransclem22  39149  etransclem24  39151  etransclem35  39162  sge0pnfval  39266  isomenndlem  39420  hoicvrrex  39446  ovn0  39456  volicon0  39465  hsphoidmvle2  39475  hsphoidmvle  39476  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmvlelem2  39486  hoidmvlelem3  39487  hspmbllem1  39516  hspmbllem2  39517  volico2  39531  ovolval2lem  39533  ovnsubadd2lem  39535  ovolval4lem1  39539  vonioolem1  39571  vonioo  39573  vonicclem1  39574  vonicc  39576  1loopgrvd2  40718  1hevtxdg1  40721  1egrvtxdg1  40725  crctcsh1wlkn0lem2  41014  crctcshlem4  41023  crctcsh  41027  clwlkclwwlklem2fv1  41204  eulercrct  41410  eucrct2eupth  41413
  Copyright terms: Public domain W3C validator