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

Theorem iftrued 4043
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 4041 . 2 (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
31, 2syl 17 1 (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  ifcif 4035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-if 4036
This theorem is referenced by:  mpt2snif  6630  tz7.44-3  7368  iunfictbso  8797  ttukeylem7  9197  max0sub  11860  ifle  11861  xmulneg1  11928  xmulpnf1  11933  expnnval  12680  swrdval2  13218  swrdlend  13229  swrd0  13232  swrdccatid  13294  relexp0g  13556  max0add  13844  summolem2a  14239  prodmolem2a  14449  ef0lem  14594  rpnnen2lem3  14730  rpnnen2lem9  14736  iserodd  15324  pcmpt  15380  pcmpt2  15381  prmdvdsprmo  15530  setcepi  16507  gsumval2a  17048  mgm2nsgrplem3  17176  mulgnn  17316  pmtrprfv  17642  pmtrprfval  17676  psgnunilem1  17682  dfod2  17750  oddvds2  17752  cyggenod  18055  mplcoe1  19232  mplcoe5  19235  coe1tm  19410  coe1tmmul2fv  19415  coe1pwmulfv  19417  coe1sclmul  19419  coe1sclmul2  19421  m1detdiag  20164  mdetunilem9  20187  maducoeval2  20207  symgmatr01lem  20220  pmatcollpw3fi1lem1  20352  chpmat1dlem  20401  chfacffsupp  20422  chfacfscmul0  20424  chfacfpmmul0  20428  2ndcdisj  21011  dscmet  22128  xrsxmet  22352  cnmpt2pc  22466  xrhmeo  22484  oprpiece1res1  22489  htpycc  22518  pcoval1  22552  pcohtpylem  22558  pcoass  22563  pcorevlem  22565  ovolunlem1a  22988  ovolunlem1  22989  ovolicc2lem3  23011  ovolicc2lem4  23012  mbfi1fseqlem4  23208  mbfi1fseqlem5  23209  mbfi1fseqlem6  23210  itg2const2  23231  itg2splitlem  23238  itg2split  23239  itg2cnlem1  23251  itg2cnlem2  23252  iblss2  23295  itgspliticc  23326  ditgpos  23343  limcres  23373  plyeq0lem  23687  plypf1  23689  coeeq2  23719  dvply1  23760  aareccl  23802  dvtaylp  23845  pserdvlem2  23903  lgamgulmlem4  24475  isppw  24557  vmappw  24559  muval1  24576  dchrelbasd  24681  dchr1  24699  dchrptlem2  24707  lgsdir2  24772  lgsne0  24777  gausslemma2dlem1a  24807  gausslemma2dlem2  24809  rplogsumlem2  24891  dchrisum0flblem2  24915  dchrisum0fno1  24917  rplogsum  24933  pntrlog2bndlem5  24987  clwlkisclwwlklem2fv1  26076  eupath2  26273  partfun  28664  ofldchr  28951  psgnfzto1stlem  28987  smattl  28998  smattr  28999  smatbl  29000  1smat1  29004  madjusmdetlem1  29027  madjusmdetlem2  29028  esumpinfval  29268  eulerpartlemgs2  29575  ballotlemsgt1  29705  ballotlemsel1i  29707  ballotlemsi  29709  signswmnd  29766  signsvtn  29793  cvmliftlem10  30336  unblimceq0lem  31473  poimirlem1  32376  poimirlem2  32377  poimirlem5  32380  poimirlem6  32381  poimirlem12  32387  poimirlem17  32392  poimirlem19  32394  poimirlem20  32395  poimirlem22  32397  poimirlem23  32398  itg2addnc  32430  itg2gt0cn  32431  itgaddnclem2  32435  sdclem1  32505  cdlemefs27cl  34515  flcidc  36559  relexp01min  36820  relexpxpmin  36824  ioondisj2  38358  ioondisj1  38359  lptioo1  38496  icccncfext  38570  cncfiooicc  38577  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  dvnxpaek  38629  ditgeq3d  38653  itgsubsticclem  38664  dirkerper  38786  dirkercncflem2  38794  fourierdlem40  38837  fourierdlem65  38861  fourierdlem74  38870  fourierdlem75  38871  fourierdlem78  38874  fourierdlem81  38877  fourierdlem97  38893  fourierdlem103  38899  fourierdlem104  38900  sqwvfoura  38918  sqwvfourb  38919  fourierswlem  38920  fouriersw  38921  elaa2lem  38923  etransclem19  38943  etransclem22  38946  etransclem24  38948  etransclem35  38959  sge0pnfval  39063  isomenndlem  39217  hoicvrrex  39243  ovn0  39253  volicon0  39262  hsphoidmvle2  39272  hsphoidmvle  39273  hoidmv1lelem1  39278  hoidmv1lelem2  39279  hoidmvlelem2  39283  hoidmvlelem3  39284  hspmbllem1  39313  hspmbllem2  39314  volico2  39328  ovolval2lem  39330  ovnsubadd2lem  39332  ovolval4lem1  39336  vonioolem1  39368  vonioo  39370  vonicclem1  39371  vonicc  39373  1loopgrvd2  40713  1hevtxdg1  40716  1egrvtxdg1  40720  crctcsh1wlkn0lem2  41009  crctcshlem4  41018  crctcsh  41022  clwlkclwwlklem2fv1  41199  eulercrct  41405  eucrct2eupth  41408
  Copyright terms: Public domain W3C validator