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

Theorem mp3an1 1360
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
Hypotheses
Ref Expression
mp3an1.1  |-  ph
mp3an1.2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mp3an1  |-  ( ( ps  /\  ch )  ->  th )

Proof of Theorem mp3an1
StepHypRef Expression
1 mp3an1.1 . 2  |-  ph
2 mp3an1.2 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
323expb 1216 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
41, 3mpan 681 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    /\ w3a 991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993
This theorem is referenced by:  mp3an12  1363  mp3an1i  1366  mp3anl1  1367  mp3an  1373  mp3an2i  1378  onint  6649  wfrlem12  7073  wfrlem17  7078  tfrlem9  7129  oaord1  7278  oaword2  7280  oawordeulem  7281  oa00  7286  omword1  7300  omword2  7301  omlimcl  7305  oeoelem  7325  nnaordex  7365  enp1i  7832  unfilem2  7862  dffi3  7971  unbnn3  8190  pwcdaen  8641  ackbij1b  8695  zorn2  8962  zornn0  8964  ttukey  8974  brdom7disj  8985  brdom6disj  8986  wunex2  9189  muladd11  9829  00id  9834  mul02  9837  negsubdi  9956  mulneg1  10083  ltaddpos  10132  addge01  10152  reccl  10305  recid  10312  recid2  10313  recdiv2  10348  divdiv23zi  10388  ltmul12a  10489  lemul12a  10491  mulgt1  10492  ltmulgt11  10493  gt0div  10499  ge0div  10500  lediv12a  10527  ledivp1  10536  ltdiv23i  10559  ledivp1i  10560  ltdivp1i  10561  infm3  10596  infmrclOLD  10621  nngt1ne1  10664  8th4div3  10862  gtndiv  11042  nn0ind  11059  fnn0ind  11063  supminf  11279  supminfOLD  11280  xrre2  11494  qsqueeze  11523  xmulpnf1  11589  xlemul1a  11603  xrub  11626  ioorebas  11765  elfz0ubfz0  11924  expubnd  12365  le2sq2  12382  crreczi  12429  bernneq  12430  faclbnd5  12515  faclbnd6  12516  bccl  12539  hashbc  12649  ccatlid  12766  shftfval  13182  sgnp  13202  mulre  13233  sqrlem4  13358  sqrlem7  13361  sqreulem  13471  binom1p  13938  0.999...  13986  fallrisefac  14127  bpoly3  14160  fsumcube  14162  efsub  14203  efi4p  14240  sinadd  14267  cosadd  14268  cos2t  14281  cos2tsin  14282  sin01gt0  14293  cos01gt0  14294  absefib  14301  efieq1re  14302  demoivreALT  14304  rpnnen2lem4  14319  odd2np1  14414  divalglem0  14420  divalglem4  14424  divalglem9  14430  divalglem9OLD  14431  gcdcllem3  14524  gcdn0gt0  14535  gcdadd  14543  gcdmultiple  14567  algcvgblem  14585  algcvga  14587  isprm3  14682  divgcdodd  14702  coprm  14706  phibndlem  14767  opoe  14810  omoe  14811  opeo  14812  omeo  14813  pythagtriplem4  14818  pythagtriplem11  14824  pythagtriplem12  14825  pythagtriplem13  14826  pythagtriplem14  14827  infpn2  14906  1arith2  14921  vdwap0  14975  vdwap1  14976  ipolt  16454  gsumval2a  16571  f1otrspeq  17137  mplsubrglem  18712  evls1rhm  18960  cnfldneg  19043  cnflddiv  19047  cnfldmulg  19049  cnfldexp  19050  zringmulg  19096  remulg  19224  resubgval  19226  thlleval  19310  frlmsslsp  19403  neiptoptop  20196  iccordt  20279  qustgplem  21184  bl2ioo  21859  ioo2blex  21861  blssioo  21862  tgioo  21863  xrsblre  21878  iccntr  21888  icccmplem3  21891  reconnlem2  21894  opnreen  21898  iccpnfcnv  22021  cnllycmp  22033  pcoptcl  22101  ovolmge0  22479  ovolctb2  22494  ismbl2  22530  cmmbl  22537  nulmbl  22538  unmbl  22540  voliunlem1  22552  voliunlem2  22553  ioombl1  22564  opnmbllem  22608  mbfima  22637  i1fsub  22715  itg1sub  22716  ellimc3  22883  limcflf  22885  dvcnvre  23020  coe1termlem  23261  dgrsub  23275  dvnply2  23289  dvnply  23290  reeff1o  23451  sinperlem  23484  sincosq1eq  23516  resinf1o  23534  logeftb  23582  logge0  23603  logdivlti  23618  efopn  23652  logtayl2  23656  loglesqrt  23747  logrec  23749  xrlimcnp  23943  ppinncl  24150  chtrpcl  24151  bposlem2  24262  bposlem8  24268  lgsdir2  24305  1lgs  24314  brbtwn2  24984  colinearalglem4  24988  ax5seglem1  25007  ax5seglem2  25008  axcontlem2  25044  axcontlem4  25046  axcontlem7  25049  iswlkg  25301  redwlklem  25384  0vgrargra  25714  isgrpoi  25975  grpo2grp  26011  imsmetlem  26371  nmcvcn  26380  ipval2  26392  lnocoi  26447  nmlno0lem  26483  nmblolbii  26489  blometi  26493  blocnilem  26494  blocni  26495  ipasslem1  26521  ipasslem2  26522  ipasslem4  26524  ipasslem5  26525  ipasslem8  26527  ipblnfi  26546  ip2eqi  26547  ubthlem1  26561  htthlem  26619  h2hmetdval  26680  axhvcom-zf  26685  axhis1-zf  26696  axhis4-zf  26699  hvm1neg  26734  hvsub4  26739  hvsubass  26746  hvsubdistr2  26752  hv2times  26763  hvsubcan  26776  hvsubcan2  26777  his2sub  26794  norm-i  26831  normpyc  26848  hhip  26879  hhph  26880  norm1exi  26952  hhssabloi  26962  hhssnv  26964  hhshsslem2  26968  hhssmetdval  26978  shscli  27019  shunssi  27070  shsleji  27072  shsidmi  27086  spanunsni  27281  h1datomi  27283  spansncvi  27354  pjss2i  27382  pjssmii  27383  pjocini  27400  homulid2  27502  honegdi  27511  ho2times  27521  nmopge0  27613  nmopgt0  27614  nmfnge0  27629  lnopaddi  27673  lnopmuli  27674  lnopsubi  27676  hmopbdoptHIL  27690  nmbdoplbi  27726  nmcoplbi  27730  nmophmi  27733  lnopconi  27736  lnfnaddi  27745  lnfnsubi  27748  nmbdfnlbi  27751  nmcfnlbi  27754  lnfnconi  27757  imaelshi  27760  cnlnadjlem2  27770  cnlnadjlem7  27775  nmoptrii  27796  nmopcoi  27797  adjcoi  27802  nmopcoadji  27803  bracnlnval  27816  leopmul  27836  opsqrlem1  27842  opsqrlem6  27847  hmopidmpji  27854  sto2i  27939  strlem1  27952  atcveq0  28050  atcv0eq  28081  atomli  28084  atcvati  28088  atcvat3i  28098  cdjreui  28134  cdj1i  28135  xdiv0  28447  xdivpnfrp  28451  mhmhmeotmd  28782  rezh  28824  qqhucn  28845  blscon  30016  cnllyscon  30017  ghomgrpilem2  30353  ghomsn  30355  sinccvglem  30365  frrlem11  30575  nobndlem8  30637  opnrebl2  31026  ptrecube  31985  poimirlem6  31991  poimirlem7  31992  poimirlem29  32014  poimirlem30  32015  opnmbllem0  32021  mblfinlem3  32024  mblfinlem4  32025  ismblfin  32026  voliunnfl  32029  ftc1anclem5  32066  ftc1anclem6  32067  ftc1anclem7  32068  ftc1anclem8  32069  ftc1anc  32070  heiborlem7  32194  rrnequiv  32212  ismrer1  32215  cnaddcom  32583  mapco2  35602  mzpaddmpt  35628  mzpmulmpt  35629  zindbi  35839  mpaaeu  36061  eel000cT  37126  eel0TT  37127  eel012  37131  wrdred1hash  38959  fusgrfis  39446  zringsubgval  40460  aacllem  40813
  Copyright terms: Public domain W3C validator