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  714  mp3an3  1453  merco2  1701  equs4v  1976  equcomiv  1987  equcomi  1990  equvinv  2003  equviniva  2004  aeveq  2024  spimt  2289  equs4  2326  axc15  2339  2ax6elem  2477  pm13.183  3376  sbcth  3483  sbcth2  3556  ssun3  3811  ssun4  3812  uneqdifeqOLD  4091  ralf0OLD  4112  elpreqprlem  4426  uniintsn  4546  rext  4946  exss  4961  propssopi  5000  uniopel  5007  wefrc  5137  relopabi  5278  relop  5305  dmrnssfld  5416  iss  5482  sofld  5616  ordun  5867  nfunv  5959  funimass2  6010  fvbr0  6253  fvmptg  6319  funsndifnop  6456  fovcl  6807  ov3  6839  elovmpt2  6921  limsssuc  7092  tfisi  7100  finds1  7137  frxp  7332  wfrlem5  7464  wfrlem16  7475  dfrecs3  7514  tfrlem1  7517  oaordi  7671  oaword2  7678  omeulem1  7707  oeworde  7718  oelim2  7720  nnaordi  7743  oaabs2  7770  0domg  8128  limenpsi  8176  enp1i  8236  findcard2  8241  ordunifi  8251  fidomdm  8284  dffi3  8378  oismo  8486  wdom2d  8526  wdomima2g  8532  suc11reg  8554  elom3  8583  cantnfval2  8604  rankunb  8751  rankval4  8768  karden  8796  cardsn  8833  cardlim  8836  cardprclem  8843  fseqdom  8887  dfac12lem3  9005  kmlem2  9011  kmlem10  9019  cflim2  9123  cfslb2n  9128  fin23lem27  9188  axcc3  9298  axcc4  9299  acncc  9300  domtriomlem  9302  axdclem2  9380  imadomg  9394  alephval2  9432  alephreg  9442  axextnd  9451  fpwwe2lem10  9499  pwfseq  9524  gch2  9535  axgroth3  9691  inaprc  9696  nlt1pi  9766  indpi  9767  1re  10077  mul02lem2  10251  addid1  10254  fimaxre  11006  supaddc  11028  supmul1  11030  inelr  11048  rimul  11049  nnge1  11084  zneo  11498  ltweuz  12800  hashrabsn1  13201  hashf1lem2  13278  hash2pwpr  13296  climuni  14327  fsum2d  14546  fsumabs  14577  fsumrlim  14587  fsumo1  14588  fsumiun  14597  fprod2d  14755  efne0  14871  ruclem13  15015  dvdslelem  15078  mod2eq1n2dvds  15118  nn0o1gt2  15144  divalglem0  15163  lcmfnnval  15384  prmreclem2  15668  prmreclem3  15669  mreexexd  16355  mreexexdOLD  16356  coaval  16765  xpcco  16870  pltirr  17010  frgpnabllem1  18322  ablfac1eulem  18517  mdetunilem9  20474  mretopd  20944  fiuncmp  21255  ptcmpfi  21664  filtop  21706  supnfcls  21871  flimfnfcls  21879  alexsubALTlem2  21899  alexsubALTlem4  21901  trust  22080  rectbntr0  22682  fsumcn  22720  ovoliunlem3  23318  ovolicc2lem4  23334  dyadmax  23412  vitali  23427  itgfsum  23638  dvmptfsum  23783  fta1g  23972  fta1  24108  aannenlem1  24128  aalioulem3  24134  logltb  24391  logdmn0  24431  ang180lem2  24585  angpined  24602  mumullem2  24951  lgsqrmodndvds  25123  gausslemma2dlem0i  25134  2lgs  25177  dchrisum0re  25247  chpdifbnd  25289  pntrlog2bnd  25318  pntibndlem3  25326  pnt3  25346  nbgrval  26274  vtxdginducedm1fi  26496  upgrewlkle2  26558  hiidge0  28083  chsupval  28322  chsupcl  28327  chsupss  28329  ococin  28395  chsupval2  28397  ssjo  28434  h1de2i  28540  pjss2i  28667  pjssmii  28668  sto2i  29224  stge1i  29225  stle0i  29226  stlei  29227  stlesi  29228  stm1i  29230  staddi  29233  stadd3i  29235  golem1  29258  stcltrlem1  29263  mdexchi  29322  chirred  29382  atabsi  29388  abrexdomjm  29471  iocinif  29671  voliune  30420  volfiniune  30421  probdif  30610  bnj849  31121  kur14lem9  31322  dford5  31734  frrlem5  31909  nofv  31935  nomaxmo  31972  noprc  32020  sscoid  32145  limsucncmpi  32569  bj-peirce  32668  bj-sbex  32751  bj-alequexv  32780  bj-axc10  32832  bj-alequex  32833  bj-spimtv  32843  bj-exlimmpi  33030  bj-restpw  33170  finxpreclem4  33361  wl-embant  33423  wl-orel12  33424  wl-euequ1f  33486  poimirlem9  33548  abrexdom  33655  heiborlem10  33749  dvrunz  33883  iss2  34252  equcomi1  34504  ax12eq  34545  ax12el  34546  ax12inda  34552  ax12v2-o  34553  cvrnrefN  34887  pmod1i  35452  pmodN  35454  osumcllem11N  35570  pexmidlem8N  35581  pl42lem3N  35585  cdleme18b  35897  dochexmidlem8  37073  pellexlem3  37712  pell1234qrne0  37734  hbtlem6  38016  or3or  38636  isotone1  38663  isotone2  38664  clsf2  38741  radcnvrat  38830  3impexpbicom  39002  sb5ALT  39048  eexinst01  39049  ax6e2eq  39090  sineq0ALT  39487  fzisoeu  39828  ovnsubaddlem2  41106  funressnfv  41529  faovcl  41601  sprsymrelfo  42072  cznnring  42281  zlmodzxznm  42611  elbigolo1  42676  dignn0flhalflem1  42734  nn0sumshdig  42742  vsetrec  42774
  Copyright terms: Public domain W3C validator