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

Theorem mpi 20
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 𝜓
mpi.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mpi (𝜑𝜒)

Proof of Theorem mpi
StepHypRef Expression
1 mpi.1 . . 3 𝜓
21a1i 11 . 2 (𝜑𝜓)
3 mpi.2 . 2 (𝜑 → (𝜓𝜒))
42, 3mpd 15 1 (𝜑𝜒)
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  21  syl6mpi  67  mp2ani  681  mp3an3  1567  merco2  1816  equs4v  2099  equcomiv  2110  equcomi  2113  equvinvOLD  2127  equvinva  2128  aeveq  2150  spimt  2427  equs4  2457  axc15  2471  2ax6elem  2609  pm13.183  3539  sbcth  3648  sbcth2  3718  ssun3  3977  ssun4  3978  elpreqprlem  4588  uniintsn  4706  rext  5106  exss  5121  snopeqop  5160  propssopi  5163  uniopel  5171  opthhausdorff  5172  opthhausdorff0  5173  wefrc  5305  relopabi  5447  relop  5474  dmrnssfld  5585  iss  5652  sofld  5792  ordun  6042  nfunv  6134  funimass2  6183  fvbr0  6435  fvmptg  6501  funsndifnop  6640  fovcl  6995  ov3  7027  elovmpt2  7109  limsssuc  7280  tfisi  7288  finds1  7325  frxp  7521  wfrlem5  7655  wfrlem16  7666  dfrecs3  7705  tfrlem1  7708  oaordi  7863  oaword2  7870  omeulem1  7899  oeworde  7910  oelim2  7912  nnaordi  7935  oaabs2  7962  0domg  8326  limenpsi  8374  enp1i  8434  findcard2  8439  ordunifi  8449  fidomdm  8482  dffi3  8576  oismo  8684  wdom2d  8724  wdomima2g  8730  epnsym  8751  suc11reg  8763  elom3  8792  cantnfval2  8813  rankunb  8960  rankval4  8977  karden  9005  cardsn  9078  cardlim  9081  cardprclem  9088  fseqdom  9132  dfac12lem3  9252  kmlem2  9258  kmlem10  9266  cflim2  9370  cfslb2n  9375  fin23lem27  9435  axcc3  9545  axcc4  9546  acncc  9547  domtriomlem  9549  axdclem2  9627  imadomg  9641  alephval2  9679  alephreg  9689  axextnd  9698  fpwwe2lem10  9746  pwfseq  9771  gch2  9782  axgroth3  9938  inaprc  9943  nlt1pi  10013  indpi  10014  1re  10325  mul02lem2  10498  addid1  10501  fimaxre  11253  supaddc  11275  supmul1  11277  inelr  11295  rimul  11296  nnge1  11332  zneo  11726  ltweuz  12984  hashrabsn1  13381  hashf1lem2  13457  hash2pwpr  13475  climuni  14506  fsum2d  14725  fsumabs  14755  fsumrlim  14765  fsumo1  14766  fsumiun  14775  fprod2d  14932  efne0  15047  ruclem13  15191  dvdslelem  15254  mod2eq1n2dvds  15291  nn0o1gt2  15317  divalglem0  15336  lcmfnnval  15556  prmreclem2  15838  prmreclem3  15839  mreexexd  16513  coaval  16922  xpcco  17028  pltirr  17168  frgpnabllem1  18477  ablfac1eulem  18673  mdetunilem9  20637  mretopd  21110  fiuncmp  21421  ptcmpfi  21830  filtop  21872  supnfcls  22037  flimfnfcls  22045  alexsubALTlem2  22065  alexsubALTlem4  22067  trust  22246  rectbntr0  22848  fsumcn  22886  ovoliunlem3  23485  ovolicc2lem4  23501  dyadmax  23579  vitali  23594  itgfsum  23807  dvmptfsum  23952  fta1g  24141  fta1  24277  aannenlem1  24297  aalioulem3  24303  logltb  24560  logdmn0  24600  ang180lem2  24754  angpined  24771  mumullem2  25120  lgsqrmodndvds  25292  gausslemma2dlem0i  25303  2lgs  25346  dchrisum0re  25416  chpdifbnd  25458  pntrlog2bnd  25487  pntibndlem3  25495  pnt3  25515  nbgrval  26445  vtxdginducedm1fi  26668  upgrewlkle2  26730  hiidge0  28283  chsupval  28522  chsupcl  28527  chsupss  28529  ococin  28595  chsupval2  28597  ssjo  28634  h1de2i  28740  pjss2i  28867  pjssmii  28868  sto2i  29424  stge1i  29425  stle0i  29426  stlei  29427  stlesi  29428  stm1i  29430  staddi  29433  stadd3i  29435  golem1  29458  stcltrlem1  29463  mdexchi  29522  chirred  29582  atabsi  29588  abrexdomjm  29670  iocinif  29870  voliune  30617  volfiniune  30618  probdif  30807  bnj849  31318  kur14lem9  31519  dford5  31930  frrlem5  32105  nofv  32131  nomaxmo  32168  noprc  32216  sscoid  32341  limsucncmpi  32761  bj-peirce  32859  bj-sbex  32942  bj-alequexv  32970  bj-axc10  33022  bj-alequex  33023  bj-spimtv  33033  bj-exlimvmpi  33213  bj-exlimmpi  33214  bj-restpw  33356  finxpreclem4  33547  wl-embant  33609  wl-orel12  33610  wl-euequif  33670  poimirlem9  33731  abrexdom  33837  heiborlem10  33930  dvrunz  34064  iss2  34425  equcomi1  34679  ax12eq  34720  ax12el  34721  ax12inda  34727  ax12v2-o  34728  cvrnrefN  35062  pmod1i  35628  pmodN  35630  osumcllem11N  35746  pexmidlem8N  35757  pl42lem3N  35761  cdleme18b  36073  dochexmidlem8  37248  pellexlem3  37897  pell1234qrne0  37919  hbtlem6  38200  or3or  38819  isotone1  38846  isotone2  38847  clsf2  38924  radcnvrat  39013  3impexpbicom  39183  sb5ALT  39229  eexinst01  39230  ax6e2eq  39271  sineq0ALT  39667  fzisoeu  39995  ovnsubaddlem2  41267  funressnfv  41662  faovcl  41789  sprsymrelfo  42315  cznnring  42524  zlmodzxznm  42854  elbigolo1  42919  dignn0flhalflem1  42977  nn0sumshdig  42985  vsetrec  43017
  Copyright terms: Public domain W3C validator