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

Theorem iftrued 3914
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 3912 . 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 1437   ifcif 3906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-if 3907
This theorem is referenced by:  mpt2snif  6395  tz7.44-3  7125  iunfictbso  8534  ttukeylem7  8934  max0sub  11478  ifle  11479  xmulneg1  11544  xmulpnf1  11549  expnnval  12261  swrdval2  12750  swrdlend  12761  swrd0  12764  swrdccatid  12827  relexp0g  13053  max0add  13341  summolem2a  13748  prodmolem2a  13955  ef0lem  14100  rpnnen2lem3  14236  rpnnen2lem9  14242  iserodd  14737  pcmpt  14789  pcmpt2  14790  prmdvdsprmo  14952  prmdvdsprmorOLD  14967  setcepi  15927  gsumval2a  16466  mgm2nsgrplem3  16598  mulgnn  16708  pmtrprfv  17038  pmtrprfval  17072  psgnunilem1  17078  dfod2  17146  oddvds2  17148  cyggenod  17447  mplcoe1  18617  mplcoe5  18620  coe1tm  18794  coe1tmmul2fv  18799  coe1pwmulfv  18801  coe1sclmul  18803  coe1sclmul2  18805  m1detdiag  19546  mdetunilem9  19569  maducoeval2  19589  symgmatr01lem  19602  pmatcollpw3fi1lem1  19734  chpmat1dlem  19783  chfacffsupp  19804  chfacfscmul0  19806  chfacfpmmul0  19810  2ndcdisj  20395  dscmet  21511  xrsxmet  21731  cnmpt2pc  21845  xrhmeo  21863  oprpiece1res1  21868  htpycc  21897  pcoval1  21930  pcohtpylem  21936  pcoass  21941  pcorevlem  21943  ovolunlem1a  22323  ovolunlem1  22324  ovolicc2lem3  22346  ovolicc2lem4OLD  22347  ovolicc2lem4  22348  mbfi1fseqlem4  22550  mbfi1fseqlem5  22551  mbfi1fseqlem6  22552  itg2const2  22573  itg2splitlem  22580  itg2split  22581  itg2cnlem1  22593  itg2cnlem2  22594  iblss2  22637  itgspliticc  22668  ditgpos  22685  limcres  22715  plyeq0lem  23029  plypf1  23031  coeeq2  23061  dvply1  23102  aareccl  23144  dvtaylp  23187  pserdvlem2  23245  lgamgulmlem4  23819  isppw  23901  vmappw  23903  muval1  23920  dchrelbasd  24027  dchr1  24045  dchrptlem2  24053  lgsdir2  24116  lgsne0  24121  rplogsumlem2  24183  dchrisum0flblem2  24207  dchrisum0fno1  24209  rplogsum  24225  pntrlog2bndlem5  24279  clwlkisclwwlklem2fv1  25352  eupath2  25550  gxpval  25829  partfun  28115  ofldchr  28413  psgnfzto1stlem  28449  smattl  28460  smattr  28461  smatbl  28462  1smat1  28466  madjusmdetlem1  28489  madjusmdetlem2  28490  esumpinfval  28730  eulerpartlemgs2  29036  ballotlemsgt1  29166  ballotlemsel1i  29168  ballotlemsi  29170  signswmnd  29231  signsvtn  29258  cvmliftlem10  29802  poimirlem1  31645  poimirlem2  31646  poimirlem5  31649  poimirlem6  31650  poimirlem12  31656  poimirlem17  31661  poimirlem19  31663  poimirlem20  31664  poimirlem22  31666  poimirlem23  31667  itg2addnc  31700  itg2gt0cn  31701  itgaddnclem2  31705  sdclem1  31776  cdlemefs27cl  33689  flcidc  35743  relexp01min  35948  relexpxpmin  35952  ioondisj2  37178  ioondisj1  37179  lptioo1  37288  icccncfext  37341  cncfiooicc  37348  ioodvbdlimc1lem2  37380  ioodvbdlimc2lem  37382  dvnxpaek  37390  ditgeq3d  37414  itgsubsticclem  37425  dirkerper  37531  dirkercncflem2  37539  fourierdlem40  37582  fourierdlem65  37607  fourierdlem74  37616  fourierdlem75  37617  fourierdlem78  37620  fourierdlem81  37623  fourierdlem97  37639  fourierdlem103  37645  fourierdlem104  37646  sqwvfoura  37664  sqwvfourb  37665  fourierswlem  37666  fouriersw  37667  elaa2lem  37669  etransclem19  37689  etransclem22  37692  etransclem24  37694  etransclem35  37705  sge0pnfval  37753
  Copyright terms: Public domain W3C validator