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

Theorem iftrued 3880
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 3878 . 2  |-  ( ch 
->  if ( ch ,  A ,  B )  =  A )
31, 2syl 17 1  |-  ( ph  ->  if ( ch ,  A ,  B )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1452   ifcif 3872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-if 3873
This theorem is referenced by:  mpt2snif  6409  tz7.44-3  7144  iunfictbso  8563  ttukeylem7  8963  max0sub  11512  ifle  11513  xmulneg1  11580  xmulpnf1  11585  expnnval  12313  swrdval2  12830  swrdlend  12841  swrd0  12844  swrdccatid  12907  relexp0g  13162  max0add  13450  summolem2a  13858  prodmolem2a  14065  ef0lem  14210  rpnnen2lem3  14346  rpnnen2lem9  14352  iserodd  14864  pcmpt  14916  pcmpt2  14917  prmdvdsprmo  15079  prmdvdsprmorOLD  15094  setcepi  16061  gsumval2a  16600  mgm2nsgrplem3  16732  mulgnn  16842  pmtrprfv  17172  pmtrprfval  17206  psgnunilem1  17212  dfod2  17293  oddvds2  17295  cyggenod  17597  mplcoe1  18766  mplcoe5  18769  coe1tm  18943  coe1tmmul2fv  18948  coe1pwmulfv  18950  coe1sclmul  18952  coe1sclmul2  18954  m1detdiag  19699  mdetunilem9  19722  maducoeval2  19742  symgmatr01lem  19755  pmatcollpw3fi1lem1  19887  chpmat1dlem  19936  chfacffsupp  19957  chfacfscmul0  19959  chfacfpmmul0  19963  2ndcdisj  20548  dscmet  21665  xrsxmet  21905  cnmpt2pc  22034  xrhmeo  22052  oprpiece1res1  22057  htpycc  22089  pcoval1  22122  pcohtpylem  22128  pcoass  22133  pcorevlem  22135  ovolunlem1a  22527  ovolunlem1  22528  ovolicc2lem3  22550  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  mbfi1fseqlem4  22755  mbfi1fseqlem5  22756  mbfi1fseqlem6  22757  itg2const2  22778  itg2splitlem  22785  itg2split  22786  itg2cnlem1  22798  itg2cnlem2  22799  iblss2  22842  itgspliticc  22873  ditgpos  22890  limcres  22920  plyeq0lem  23243  plypf1  23245  coeeq2  23275  dvply1  23316  aareccl  23361  dvtaylp  23404  pserdvlem2  23462  lgamgulmlem4  24036  isppw  24120  vmappw  24122  muval1  24139  dchrelbasd  24246  dchr1  24264  dchrptlem2  24272  lgsdir2  24335  lgsne0  24340  rplogsumlem2  24402  dchrisum0flblem2  24426  dchrisum0fno1  24428  rplogsum  24444  pntrlog2bndlem5  24498  clwlkisclwwlklem2fv1  25589  eupath2  25787  gxpval  26068  partfun  28353  ofldchr  28651  psgnfzto1stlem  28687  smattl  28698  smattr  28699  smatbl  28700  1smat1  28704  madjusmdetlem1  28727  madjusmdetlem2  28728  esumpinfval  28968  eulerpartlemgs2  29286  ballotlemsgt1  29416  ballotlemsel1i  29418  ballotlemsi  29420  ballotlemsgt1OLD  29454  ballotlemsel1iOLD  29456  ballotlemsiOLD  29458  signswmnd  29518  signsvtn  29545  cvmliftlem10  30089  poimirlem1  32005  poimirlem2  32006  poimirlem5  32009  poimirlem6  32010  poimirlem12  32016  poimirlem17  32021  poimirlem19  32023  poimirlem20  32024  poimirlem22  32026  poimirlem23  32027  itg2addnc  32060  itg2gt0cn  32061  itgaddnclem2  32065  sdclem1  32136  cdlemefs27cl  34051  flcidc  36111  relexp01min  36376  relexpxpmin  36380  ioondisj2  37685  ioondisj1  37686  lptioo1  37809  icccncfext  37862  cncfiooicc  37869  ioodvbdlimc1lem2  37901  ioodvbdlimc1lem2OLD  37903  ioodvbdlimc2lem  37905  ioodvbdlimc2lemOLD  37906  dvnxpaek  37914  ditgeq3d  37938  itgsubsticclem  37949  dirkerper  38070  dirkercncflem2  38078  fourierdlem40  38122  fourierdlem65  38147  fourierdlem74  38156  fourierdlem75  38157  fourierdlem78  38160  fourierdlem81  38163  fourierdlem97  38179  fourierdlem103  38185  fourierdlem104  38186  sqwvfoura  38204  sqwvfourb  38205  fourierswlem  38206  fouriersw  38207  elaa2lem  38209  elaa2lemOLD  38210  etransclem19  38230  etransclem22  38233  etransclem24  38235  etransclem35  38246  sge0pnfval  38329  isomenndlem  38470  hoicvrrex  38496  ovn0  38506  volicon0  38515  hsphoidmvle2  38525  hsphoidmvle  38526  hoidmv1lelem1  38531  hoidmv1lelem2  38532  hoidmvlelem2  38536  hoidmvlelem3  38537  hspmbllem1  38566  hspmbllem2  38567  volico2  38581  ovolval2lem  38583  ovnsubadd2lem  38585  ovolval4lem1  38589  1loopgrvd2  39725  1hevtxdg1  39728  1egrvtxdg1  39732  crctcsh1wlkn0lem2  39989  crctcshlem4  39998  crctcsh  40002  eulercrct  40154  eucrct2eupth  40157
  Copyright terms: Public domain W3C validator