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

Step	Hyp	Ref	Expression
1		mpi.1	. . 3 ⊢ 𝜓
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝜓)
3		mpi.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	mpd 15	1 ⊢ (𝜑 → 𝜒)

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  65  mp2ani  710  mp3an3  1405  merco2  1652  equs4v  1917  equcomiv  1928  equcomi  1931  equvinv  1946  equviniva  1947  equvinivOLD  1948  aeveq  1969  aevOLD  2148  spimt  2241  equs4  2278  axc15  2291  ax12v2OLD  2330  2ax6elem  2437  pm13.183  3313  sbcth  3417  sbcth2  3489  ssun3  3740  ssun4  3741  uneqdifeqOLD  4010  ralf0OLD  4031  elpreqprlem  4333  uniintsn  4449  rext  4843  exss  4858  propssopi  4896  uniopel  4903  wefrc  5032  relopabi  5167  relop  5194  dmrnssfld  5305  iss  5367  sofld  5500  ordun  5746  nfunv  5835  funimass2  5886  fvbr0  6125  fvmptg  6189  funsndifnop  6321  fovcl  6663  ov3  6695  elovmpt2  6777  limsssuc  6942  tfisi  6950  finds1  6987  frxp  7174  wfrlem5  7306  wfrlem16  7317  dfrecs3  7356  tfrlem1  7359  oaordi  7513  oaword2  7520  omeulem1  7549  oeworde  7560  oelim2  7562  nnaordi  7585  oaabs2  7612  0domg  7972  limenpsi  8020  enp1i  8080  findcard2  8085  ordunifi  8095  fidomdm  8128  dffi3  8220  oismo  8328  wdom2d  8368  wdomima2g  8374  suc11reg  8399  elom3  8428  cantnfval2  8449  rankunb  8596  rankval4  8613  karden  8641  cardsn  8678  cardlim  8681  cardprclem  8688  fseqdom  8732  dfac12lem3  8850  kmlem2  8856  kmlem10  8864  cflim2  8968  cfslb2n  8973  fin23lem27  9033  axcc3  9143  axcc4  9144  acncc  9145  domtriomlem  9147  axdclem2  9225  imadomg  9237  alephval2  9273  alephreg  9283  axextnd  9292  fpwwe2lem10  9340  pwfseq  9365  gch2  9376  axgroth3  9532  inaprc  9537  nlt1pi  9607  indpi  9608  1re  9918  mul02lem2  10092  addid1  10095  fimaxre  10847  supaddc  10867  supmul1  10869  inelr  10887  rimul  10888  nnge1  10923  zneo  11336  ltweuz  12622  hashrabsn1  13024  hashf1lem2  13097  hash2pwpr  13115  climuni  14131  fsum2d  14344  fsumabs  14374  fsumrlim  14384  fsumo1  14385  fsumiun  14394  fprod2d  14550  efne0  14666  ruclem13  14810  dvdslelem  14869  mod2eq1n2dvds  14909  nn0o1gt2  14935  divalglem0  14954  lcmfnnval  15175  prmreclem2  15459  prmreclem3  15460  mreexexd  16131  mreexexdOLD  16132  coaval  16541  xpcco  16646  pltirr  16786  frgpnabllem1  18099  ablfac1eulem  18294  mdetunilem9  20245  mretopd  20706  fiuncmp  21017  ptcmpfi  21426  filtop  21469  supnfcls  21634  flimfnfcls  21642  alexsubALTlem2  21662  alexsubALTlem4  21664  trust  21843  rectbntr0  22443  fsumcn  22481  ovoliunlem3  23079  ovolicc2lem4  23095  dyadmax  23172  vitali  23188  itgfsum  23399  dvmptfsum  23542  fta1g  23731  fta1  23867  aannenlem1  23887  aalioulem3  23893  logltb  24150  logdmn0  24186  ang180lem2  24340  angpined  24357  mumullem2  24706  lgsqrmodndvds  24878  gausslemma2dlem0i  24889  2lgs  24932  dchrisum0re  25002  chpdifbnd  25044  pntrlog2bnd  25073  pntibndlem3  25081  pnt3  25101  nbgraop  25952  isuvtx  26016  0eusgraiff0rgra  26466  frgrancvvdeqlem4  26560  hiidge0  27339  chsupval  27578  chsupcl  27583  chsupss  27585  ococin  27651  chsupval2  27653  ssjo  27690  h1de2i  27796  pjss2i  27923  pjssmii  27924  sto2i  28480  stge1i  28481  stle0i  28482  stlei  28483  stlesi  28484  stm1i  28486  staddi  28489  stadd3i  28491  golem1  28514  stcltrlem1  28519  mdexchi  28578  chirred  28638  atabsi  28644  rmoeqALT  28711  abrexdomjm  28729  iocinif  28933  voliune  29619  volfiniune  29620  probdif  29809  bnj849  30249  kur14lem9  30450  frrlem5  31028  nofv  31054  noprc  31080  sscoid  31190  limsucncmpi  31614  bj-peirce  31713  bj-sbex  31815  bj-axc10  31894  bj-alequex  31895  bj-spimtv  31905  bj-exlimmpi  32097  bj-restpw  32226  finxpreclem4  32407  wl-embant  32472  wl-orel12  32473  wl-euequ1f  32535  poimirlem9  32588  abrexdom  32695  heiborlem10  32789  dvrunz  32923  equcomi1  33203  ax12eq  33244  ax12el  33245  ax12inda  33251  ax12v2-o  33252  cvrnrefN  33587  pmod1i  34152  pmodN  34154  osumcllem11N  34270  pexmidlem8N  34281  pl42lem3N  34285  cdleme18b  34597  dochexmidlem8  35774  pellexlem3  36413  pell1234qrne0  36435  hbtlem6  36718  or3or  37339  isotone1  37366  isotone2  37367  clsf2  37444  radcnvrat  37535  3impexpbicom  37706  sb5ALT  37752  eexinst01  37753  ax6e2eq  37794  sineq0ALT  38195  fzisoeu  38455  ovnsubaddlem2  39461  funressnfv  39857  faovcl  39929  nbgrval  40560  upgrewlkle2  40808  frgrncvvdeqlem4  41472  cznnring  41748  zlmodzxznm  42080  elbigolo1  42149  dignn0flhalflem1  42207  nn0sumshdig  42215  vsetrec  42245