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

Theorem mpi 21
Description: A nested modus ponens inference. Inference associated with com12 32. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Stefan Allan, 20-Mar-2006.)
Hypotheses
Ref Expression
mpi.1  |-  ps
mpi.2  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
mpi  |-  ( ph  ->  ch )

Proof of Theorem mpi
StepHypRef Expression
1 mpi.1 . . 3  |-  ps
21a1i 11 . 2  |-  ( ph  ->  ps )
3 mpi.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  mpisyl  22  syl6mpi  64  mp2ani  682  mp3an3  1349  merco2  1615  equs4v  1838  equcomi  1845  equviniv  1855  19.8aOLD  1911  aev  2001  spimt  2061  equs4  2090  ax12v2  2139  2ax6elem  2245  pm13.183  3218  sbcth  3320  sbcth2  3389  ssun3  3637  ssun4  3638  uneqdifeq  3890  ralf0  3910  uniintsn  4296  rext  4670  exss  4685  uniopel  4725  wefrc  4848  relop  5005  dmrnssfld  5113  iss  5172  sofld  5304  relcoi1OLD  5385  ordun  5543  nfunv  5632  funimass2  5675  fvbr0  5902  fvmptg  5962  fovcl  6415  ov3  6447  elovmpt2  6528  limsssuc  6691  tfisi  6699  finds1  6736  frxp  6917  wfrlem5  7048  wfrlem16  7059  dfrecs3  7099  tfrlem1  7102  oaordi  7255  oaword2  7262  omeulem1  7291  oeworde  7302  oelim2  7304  nnaordi  7327  oaabs2  7354  0domg  7705  limenpsi  7753  enp1i  7812  findcard2  7817  ordunifi  7827  fidomdm  7859  dffi3  7951  oismo  8055  wdom2d  8095  wdomima2g  8101  suc11reg  8124  elom3  8153  cantnfval2  8173  rankunb  8320  rankval4  8337  karden  8365  cardsn  8402  cardlim  8405  cardprclem  8412  fseqdom  8455  dfac12lem3  8573  kmlem2  8579  kmlem10  8587  cflim2  8691  cfslb2n  8696  fin23lem27  8756  axcc3  8866  axcc4  8867  acncc  8868  domtriomlem  8870  axdclem2  8948  imadomg  8960  alephval2  8995  alephreg  9005  axextnd  9014  fpwwe2lem10  9063  pwfseq  9088  gch2  9099  axgroth3  9255  inaprc  9260  nlt1pi  9330  indpi  9331  1re  9641  mul02lem2  9809  addid1  9812  fimaxre  10551  supaddc  10574  supmul1  10576  inelr  10599  rimul  10600  nnge1  10635  zneo  11018  ltweuz  12172  hashrabsn1  12550  hashf1lem2  12614  hash2pwpr  12628  climuni  13594  fsum2d  13810  fsumabs  13839  fsumrlim  13849  fsumo1  13850  fsumiun  13859  fprod2d  14013  efne0  14129  ruclem13  14272  dvdslelem  14327  divalglem0  14349  lcmfnnval  14565  lcmfnnvalOLD  14568  prmreclem2  14824  prmreclem3  14825  mreexexd  15505  coaval  15914  xpcco  16019  pltirr  16160  frgpnabllem1  17444  ablfac1eulem  17640  mdetunilem9  19576  mretopd  20039  fiuncmp  20350  ptcmpfi  20759  filtop  20801  supnfcls  20966  flimfnfcls  20974  alexsubALTlem2  20994  alexsubALTlem4  20996  trust  21175  rectbntr0  21761  fsumcn  21798  ovoliunlem3  22335  ovolicc2lem4  22351  dyadmax  22433  vitali  22448  itgfsum  22661  dvmptfsum  22804  fta1g  22993  fta1  23129  aannenlem1  23149  aalioulem3  23155  logltb  23414  logdmn0  23450  ang180lem2  23604  angpined  23621  mumullem2  23970  dchrisum0re  24214  chpdifbnd  24256  pntrlog2bnd  24285  pntibndlem3  24293  pnt3  24313  nbgraop  24996  isuvtx  25061  0eusgraiff0rgra  25512  frgrancvvdeqlem4  25606  dvrunz  26006  hiidge0  26586  chsupval  26823  chsupcl  26828  chsupss  26830  ococin  26896  chsupval2  26898  ssjo  26935  h1de2i  27041  pjss2i  27168  pjssmii  27169  sto2i  27725  stge1i  27726  stle0i  27727  stlei  27728  stlesi  27729  stm1i  27731  staddi  27734  stadd3i  27736  golem1  27759  stcltrlem1  27764  mdexchi  27823  chirred  27883  atabsi  27889  rmoeq  27958  abrexdomjm  27977  ifbieq12d2  27998  iocinif  28199  voliune  28891  volfiniune  28892  probdif  29079  bnj849  29524  kur14lem9  29725  frrlem5  30305  nofv  30331  noprc  30355  sscoid  30465  limsucncmpi  30890  bj-alequex  31048  bj-spimtv  31058  bj-axc15v  31110  bj-exlimmpi  31262  wl-embantALT  31554  wl-orel12  31556  wl-ax12v3  31616  poimirlem9  31653  abrexdom  31761  heiborlem10  31856  ax12eq  32221  ax12el  32222  ax12inda  32228  ax12v2-o  32229  cvrnrefN  32557  pmod1i  33122  pmodN  33124  osumcllem11N  33240  pexmidlem8N  33251  pl42lem3N  33255  cdleme18b  33567  dochexmidlem8  34744  pellexlem3  35385  pell1234qrne0  35407  hbtlem6  35694  radcnvrat  36300  3impexpbicom  36471  sb5ALT  36519  eexinst01  36520  ax6e2eq  36561  sineq0ALT  36974  fzisoeu  37127  funressnfv  38020  faovcl  38092  mod2eq1n2dvds  38115  cznnring  38716  zlmodzxznm  39050  nn0o1gt2  39088  elbigolo1  39129  dignn0flhalflem1  39187  nn0sumshdig  39195
  Copyright terms: Public domain W3C validator