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

Theorem iftrued 3889
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 3887 . 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 1444   ifcif 3881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-if 3882
This theorem is referenced by:  mpt2snif  6390  tz7.44-3  7126  iunfictbso  8545  ttukeylem7  8945  max0sub  11489  ifle  11490  xmulneg1  11555  xmulpnf1  11560  expnnval  12275  swrdval2  12776  swrdlend  12787  swrd0  12790  swrdccatid  12853  relexp0g  13085  max0add  13373  summolem2a  13781  prodmolem2a  13988  ef0lem  14133  rpnnen2lem3  14269  rpnnen2lem9  14275  iserodd  14785  pcmpt  14837  pcmpt2  14838  prmdvdsprmo  15000  prmdvdsprmorOLD  15015  setcepi  15983  gsumval2a  16522  mgm2nsgrplem3  16654  mulgnn  16764  pmtrprfv  17094  pmtrprfval  17128  psgnunilem1  17134  dfod2  17215  oddvds2  17217  cyggenod  17519  mplcoe1  18689  mplcoe5  18692  coe1tm  18866  coe1tmmul2fv  18871  coe1pwmulfv  18873  coe1sclmul  18875  coe1sclmul2  18877  m1detdiag  19622  mdetunilem9  19645  maducoeval2  19665  symgmatr01lem  19678  pmatcollpw3fi1lem1  19810  chpmat1dlem  19859  chfacffsupp  19880  chfacfscmul0  19882  chfacfpmmul0  19886  2ndcdisj  20471  dscmet  21587  xrsxmet  21827  cnmpt2pc  21956  xrhmeo  21974  oprpiece1res1  21979  htpycc  22011  pcoval1  22044  pcohtpylem  22050  pcoass  22055  pcorevlem  22057  ovolunlem1a  22449  ovolunlem1  22450  ovolicc2lem3  22472  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  mbfi1fseqlem4  22676  mbfi1fseqlem5  22677  mbfi1fseqlem6  22678  itg2const2  22699  itg2splitlem  22706  itg2split  22707  itg2cnlem1  22719  itg2cnlem2  22720  iblss2  22763  itgspliticc  22794  ditgpos  22811  limcres  22841  plyeq0lem  23164  plypf1  23166  coeeq2  23196  dvply1  23237  aareccl  23282  dvtaylp  23325  pserdvlem2  23383  lgamgulmlem4  23957  isppw  24041  vmappw  24043  muval1  24060  dchrelbasd  24167  dchr1  24185  dchrptlem2  24193  lgsdir2  24256  lgsne0  24261  rplogsumlem2  24323  dchrisum0flblem2  24347  dchrisum0fno1  24349  rplogsum  24365  pntrlog2bndlem5  24419  clwlkisclwwlklem2fv1  25510  eupath2  25708  gxpval  25987  partfun  28278  ofldchr  28577  psgnfzto1stlem  28613  smattl  28624  smattr  28625  smatbl  28626  1smat1  28630  madjusmdetlem1  28653  madjusmdetlem2  28654  esumpinfval  28894  eulerpartlemgs2  29213  ballotlemsgt1  29343  ballotlemsel1i  29345  ballotlemsi  29347  ballotlemsgt1OLD  29381  ballotlemsel1iOLD  29383  ballotlemsiOLD  29385  signswmnd  29446  signsvtn  29473  cvmliftlem10  30017  poimirlem1  31941  poimirlem2  31942  poimirlem5  31945  poimirlem6  31946  poimirlem12  31952  poimirlem17  31957  poimirlem19  31959  poimirlem20  31960  poimirlem22  31962  poimirlem23  31963  itg2addnc  31996  itg2gt0cn  31997  itgaddnclem2  32001  sdclem1  32072  cdlemefs27cl  33980  flcidc  36040  relexp01min  36305  relexpxpmin  36309  ioondisj2  37589  ioondisj1  37590  lptioo1  37712  icccncfext  37765  cncfiooicc  37772  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  dvnxpaek  37817  ditgeq3d  37841  itgsubsticclem  37852  dirkerper  37958  dirkercncflem2  37966  fourierdlem40  38010  fourierdlem65  38035  fourierdlem74  38044  fourierdlem75  38045  fourierdlem78  38048  fourierdlem81  38051  fourierdlem97  38067  fourierdlem103  38073  fourierdlem104  38074  sqwvfoura  38092  sqwvfourb  38093  fourierswlem  38094  fouriersw  38095  elaa2lem  38097  elaa2lemOLD  38098  etransclem19  38118  etransclem22  38121  etransclem24  38123  etransclem35  38134  sge0pnfval  38215  isomenndlem  38351  hoicvrrex  38378  ovn0  38388  volicon0  38397  hsphoidmvle2  38407  hsphoidmvle  38408  hoidmv1lelem1  38413  hoidmv1lelem2  38414  hoidmvlelem2  38418  hoidmvlelem3  38419  hspmbllem1  38448  hspmbllem2  38449  uspgrloopvd2  39557
  Copyright terms: Public domain W3C validator