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

Theorem iftrued 3937
Description: Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
iftrued.1  |-  ( ph  ->  ch )
Assertion
Ref Expression
iftrued  |-  ( ph  ->  if ( ch ,  A ,  B )  =  A )

Proof of Theorem iftrued
StepHypRef Expression
1 iftrued.1 . 2  |-  ( ph  ->  ch )
2 iftrue 3935 . 2  |-  ( ch 
->  if ( ch ,  A ,  B )  =  A )
31, 2syl 16 1  |-  ( ph  ->  if ( ch ,  A ,  B )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398   ifcif 3929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-if 3930
This theorem is referenced by:  mpt2snif  6369  tz7.44-3  7066  iunfictbso  8486  ttukeylem7  8886  max0sub  11398  ifle  11399  xmulneg1  11464  xmulpnf1  11469  expnnval  12151  swrdval2  12636  swrdlend  12647  swrd0  12650  swrdccatid  12713  relexp0g  12939  max0add  13225  summolem2a  13619  prodmolem2a  13823  ef0lem  13896  rpnnen2lem3  14034  rpnnen2lem9  14040  iserodd  14443  pcmpt  14495  pcmpt2  14496  setcepi  15566  gsumval2a  16105  mgm2nsgrplem3  16237  mulgnn  16347  pmtrprfv  16677  pmtrprfval  16711  psgnunilem1  16717  dfod2  16785  oddvds2  16787  cyggenod  17086  mplcoe1  18322  mplcoe5  18326  coe1tm  18509  coe1tmmul2fv  18514  coe1pwmulfv  18516  coe1sclmul  18518  coe1sclmul2  18520  m1detdiag  19266  mdetunilem9  19289  maducoeval2  19309  symgmatr01lem  19322  pmatcollpw3fi1lem1  19454  chpmat1dlem  19503  chfacffsupp  19524  chfacfscmul0  19526  chfacfpmmul0  19530  2ndcdisj  20123  dscmet  21259  xrsxmet  21480  cnmpt2pc  21594  xrhmeo  21612  oprpiece1res1  21617  htpycc  21646  pcoval1  21679  pcohtpylem  21685  pcoass  21690  pcorevlem  21692  ovolunlem1a  22073  ovolunlem1  22074  ovolicc2lem3  22096  ovolicc2lem4  22097  mbfi1fseqlem4  22291  mbfi1fseqlem5  22292  mbfi1fseqlem6  22293  itg2const2  22314  itg2splitlem  22321  itg2split  22322  itg2cnlem1  22334  itg2cnlem2  22335  iblss2  22378  itgspliticc  22409  ditgpos  22426  limcres  22456  plyeq0lem  22773  plypf1  22775  coeeq2  22805  dvply1  22846  aareccl  22888  dvtaylp  22931  pserdvlem2  22989  isppw  23586  vmappw  23588  muval1  23605  dchrelbasd  23712  dchr1  23730  dchrptlem2  23738  lgsdir2  23801  lgsne0  23806  rplogsumlem2  23868  dchrisum0flblem2  23892  dchrisum0fno1  23894  rplogsum  23910  pntrlog2bndlem5  23964  clwlkisclwwlklem2fv1  24984  eupath2  25182  gxpval  25459  partfun  27744  ofldchr  28039  esumpinfval  28302  eulerpartlemgs2  28583  ballotlemsgt1  28713  ballotlemsel1i  28715  ballotlemsi  28717  signswmnd  28778  signsvtn  28805  lgamgulmlem4  28838  cvmliftlem10  29003  itg2addnc  30309  itg2gt0cn  30310  itgaddnclem2  30314  sdclem1  30476  flcidc  31364  ioondisj2  31764  ioondisj1  31765  lptioo1  31877  icccncfext  31929  cncfiooicc  31936  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  dvnxpaek  31978  ditgeq3d  32002  itgsubsticclem  32013  dirkerper  32117  dirkercncflem2  32125  fourierdlem40  32168  fourierdlem65  32193  fourierdlem74  32202  fourierdlem75  32203  fourierdlem78  32206  fourierdlem81  32209  fourierdlem97  32225  fourierdlem103  32231  fourierdlem104  32232  sqwvfoura  32250  sqwvfourb  32251  fourierswlem  32252  fouriersw  32253  elaa2lem  32255  etransclem19  32275  etransclem22  32278  etransclem24  32280  etransclem35  32291  cdlemefs27cl  36536  relexp01min  38219  relexpxpmin  38226
  Copyright terms: Public domain W3C validator