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

Theorem iftrued 4127
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 4125 . 2 (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
31, 2syl 17 1 (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  ifcif 4119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-if 4120
This theorem is referenced by:  mpt2snif  6796  tz7.44-3  7549  iunfictbso  8975  ttukeylem7  9375  max0sub  12065  ifle  12066  xmulneg1  12137  xmulpnf1  12142  expnnval  12903  swrdval2  13465  swrdlend  13477  swrd0  13480  swrdccatid  13543  relexp0g  13806  max0add  14094  summolem2a  14490  prodmolem2a  14708  ef0lem  14853  rpnnen2lem3  14989  rpnnen2lem9  14995  iserodd  15587  pcmpt  15643  pcmpt2  15644  prmdvdsprmo  15793  setcepi  16785  gsumval2a  17326  mgm2nsgrplem3  17454  mulgnn  17594  pmtrprfv  17919  pmtrprfval  17953  psgnunilem1  17959  dfod2  18027  oddvds2  18029  cyggenod  18332  mplcoe1  19513  mplcoe5  19516  coe1tm  19691  coe1tmmul2fv  19696  coe1pwmulfv  19698  coe1sclmul  19700  coe1sclmul2  19702  m1detdiag  20451  mdetunilem9  20474  maducoeval2  20494  symgmatr01lem  20507  pmatcollpw3fi1lem1  20639  chpmat1dlem  20688  chfacffsupp  20709  chfacfscmul0  20711  chfacfpmmul0  20715  2ndcdisj  21307  dscmet  22424  xrsxmet  22659  cnmpt2pc  22774  xrhmeo  22792  oprpiece1res1  22797  htpycc  22826  pcoval1  22859  pcohtpylem  22865  pcoass  22870  pcorevlem  22872  ovolunlem1a  23310  ovolunlem1  23311  ovolicc2lem3  23333  ovolicc2lem4  23334  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  mbfi1fseqlem6  23532  itg2const2  23553  itg2splitlem  23560  itg2split  23561  itg2cnlem1  23573  itg2cnlem2  23574  iblss2  23617  itgspliticc  23648  ditgpos  23665  limcres  23695  plyeq0lem  24011  plypf1  24013  coeeq2  24043  dvply1  24084  aareccl  24126  dvtaylp  24169  pserdvlem2  24227  lgamgulmlem4  24803  isppw  24885  vmappw  24887  muval1  24904  dchrelbasd  25009  dchr1  25027  dchrptlem2  25035  lgsdir2  25100  lgsne0  25105  gausslemma2dlem1a  25135  gausslemma2dlem2  25137  rplogsumlem2  25219  dchrisum0flblem2  25243  dchrisum0fno1  25245  rplogsum  25261  pntrlog2bndlem5  25315  1loopgrvd2  26455  1hevtxdg1  26458  1egrvtxdg1  26461  crctcshwlkn0lem2  26759  crctcshlem4  26768  crctcsh  26772  clwlkclwwlklem2fv1  26961  eulercrct  27220  eucrct2eupth  27223  partfun  29603  ofldchr  29942  psgnfzto1stlem  29978  pmtridfv1  29985  pmtridfv2  29986  smattl  29992  smattr  29993  smatbl  29994  1smat1  29998  madjusmdetlem1  30021  madjusmdetlem2  30022  esumpinfval  30263  eulerpartlemgs2  30570  ballotlemsgt1  30700  ballotlemsel1i  30702  ballotlemsi  30704  signswmnd  30762  signsvtn  30789  cvmliftlem10  31402  unblimceq0lem  32622  poimirlem1  33540  poimirlem2  33541  poimirlem5  33544  poimirlem6  33545  poimirlem12  33551  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem22  33561  poimirlem23  33562  itg2addnc  33594  itg2gt0cn  33595  itgaddnclem2  33599  sdclem1  33669  cdlemefs27cl  36018  flcidc  38061  relexp01min  38322  relexpxpmin  38326  ioondisj2  40032  ioondisj1  40033  lptioo1  40182  limsup10exlem  40322  icccncfext  40418  cncfiooicc  40425  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnxpaek  40475  ditgeq3d  40498  itgsubsticclem  40509  dirkerper  40631  dirkercncflem2  40639  fourierdlem40  40682  fourierdlem65  40706  fourierdlem74  40715  fourierdlem75  40716  fourierdlem78  40719  fourierdlem81  40722  fourierdlem97  40738  fourierdlem103  40744  fourierdlem104  40745  sqwvfoura  40763  sqwvfourb  40764  fourierswlem  40765  fouriersw  40766  elaa2lem  40768  etransclem19  40788  etransclem22  40791  etransclem24  40793  etransclem35  40804  sge0pnfval  40908  isomenndlem  41065  hoicvrrex  41091  ovn0  41101  volicon0  41110  hsphoidmvle2  41120  hsphoidmvle  41121  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmvlelem2  41131  hoidmvlelem3  41132  hspmbllem1  41161  hspmbllem2  41162  volico2  41176  ovolval2lem  41178  ovnsubadd2lem  41180  ovolval4lem1  41184  vonioolem1  41215  vonioo  41217  vonicclem1  41218  vonicc  41220
  Copyright terms: Public domain W3C validator