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  67  mp2ani  698  mp3an3  1451  merco2  1735  equs4v  1998  alequexv  1999  equcomiv  2012  equcomi  2015  equvinva  2028  aeveq  2055  spimt  2390  equs4  2420  axc15  2426  2ax6elem  2474  dfeumo  2536  mo4  2565  sbcth  3802  sbcth2  3883  ssun3  4179  ssun4  4180  elpreqprlem  4865  uniintsn  4984  sepexlem  5298  axprlem1  5422  axprlem2  5423  axprlem4  5425  axpr  5426  axprlem3OLD  5427  axprlem4OLD  5428  axprlem5OLD  5429  axprOLD  5430  exel  5437  rext  5452  exss  5467  snopeqop  5510  propssopi  5512  uniopel  5520  opthhausdorff  5521  opthhausdorff0  5522  wefrc  5678  relopabi  5831  relop  5860  dmrnssfld  5983  iss  6052  sofld  6206  ordun  6487  funimass2  6648  fvbr0  6934  fvmptg  7013  funsndifnop  7170  ov3  7597  elovmpo  7679  dford5  7805  limsssuc  7872  tfisi  7881  finds1  7922  frxp  8152  frxp2  8170  frxp3  8177  wfrlem5OLD  8354  wfrlem16OLD  8365  dfrecs3  8413  dfrecs3OLD  8414  tfrlem1  8417  oaordi  8585  oaword2  8592  omeulem1  8621  oeworde  8632  oelim2  8634  nnaordi  8657  oaabs2  8688  0domgOLD  9142  limenpsi  9193  dif1en  9201  dif1enOLD  9203  enp1iOLD  9315  ordunifi  9327  fidomdm  9375  dffi3  9472  oismo  9581  wdom2d  9621  wdomima2g  9627  epnsym  9650  suc11reg  9660  elom3  9689  cantnfval2  9710  rankunb  9891  rankval4  9908  karden  9936  cardsn  10010  cardlim  10013  cardprclem  10020  fseqdom  10067  dfac12lem3  10187  kmlem2  10193  kmlem10  10201  cflim2  10304  cfslb2n  10309  fin23lem27  10369  fin23lem17  10379  axcc3  10479  axcc4  10480  acncc  10481  domtriomlem  10483  axdclem2  10561  imadomg  10575  alephval2  10613  alephreg  10623  axextnd  10632  fpwwe2lem9  10680  pwfseq  10705  gch2  10716  axgroth3  10872  inaprc  10877  nlt1pi  10947  indpi  10948  1re  11262  mul02lem2  11439  addrid  11442  fimaxre  12213  fiminre  12216  supaddc  12236  supmul1  12238  inelr  12257  rimul  12258  nnge1  12295  zneo  12703  ltweuz  14003  hashrabsn1  14414  hashf1lem2  14496  hash2pwpr  14516  climuni  15589  fsum2d  15808  fsumabs  15838  fsumrlim  15848  fsumo1  15849  fsumiun  15858  fprod2d  16018  efne0  16134  ruclem13  16279  dvdslelem  16347  mod2eq1n2dvds  16385  nn0o1gt2  16419  divalglem0  16431  lcmfnnval  16662  prmreclem2  16956  prmreclem3  16957  mreexexd  17692  coaval  18114  xpcco  18229  pltirr  18381  frgpnabllem1  19892  ablfac1eulem  20093  prmgrpsimpgd  20135  mdetunilem9  22627  mretopd  23101  fiuncmp  23413  ptcmpfi  23822  filtop  23864  supnfcls  24029  flimfnfcls  24037  alexsubALTlem2  24057  alexsubALTlem4  24059  trust  24239  rectbntr0  24855  fsumcn  24895  ovoliunlem3  25540  ovolicc2lem4  25556  dyadmax  25634  vitali  25649  itgfsum  25863  dvmptfsum  26014  fta1g  26210  fta1  26351  aannenlem1  26371  aalioulem3  26377  logltb  26643  logdmn0  26683  ang180lem2  26854  angpined  26874  mumullem2  27224  lgsqrmodndvds  27398  gausslemma2dlem0i  27409  2lgs  27452  dchrisum0re  27558  chpdifbnd  27600  pntrlog2bnd  27629  pntibndlem3  27637  pnt3  27657  nofv  27703  nomaxmo  27744  nominmo  27745  noprc  27825  madebday  27939  addsproplem7  28009  negsproplem7  28067  elons2  28282  nbgrval  29354  vtxdginducedm1fi  29563  upgrewlkle2  29625  hiidge0  31118  chsupval  31355  chsupcl  31360  chsupss  31362  ococin  31428  chsupval2  31430  ssjo  31467  h1de2i  31573  pjss2i  31700  pjssmii  31701  sto2i  32257  stge1i  32258  stle0i  32259  stlei  32260  stlesi  32261  stm1i  32263  staddi  32266  stadd3i  32268  golem1  32291  stcltrlem1  32296  mdexchi  32355  chirred  32415  atabsi  32421  abrexdomjm  32527  iocinif  32784  cycpmcl  33137  elrgspnsubrunlem2  33253  voliune  34231  volfiniune  34232  probdif  34423  bnj849  34940  kur14lem9  35220  gonarlem  35400  gonar  35401  goalrlem  35402  goalr  35403  sscoid  35915  limsucncmpi  36447  bj-axc10  36785  bj-alequex  36786  bj-spimtv  36796  bj-moeub  36851  bj-exlimvmpi  36913  bj-exlimmpi  36914  bj-restpw  37094  bj-isrvec  37296  finxpreclem4  37396  domalom  37406  wl-isseteq  37507  wl-embant  37512  wl-orel12  37513  wl-euequf  37576  poimirlem9  37637  abrexdom  37738  heiborlem10  37828  dvrunz  37962  iss2  38346  equcomi1  38902  ax12eq  38943  ax12el  38944  ax12inda  38950  ax12v2-o  38951  cvrnrefN  39284  pmod1i  39851  pmodN  39853  osumcllem11N  39969  pexmidlem8N  39980  pl42lem3N  39984  cdleme18b  40295  dochexmidlem8  41470  imadomfi  42004  sticksstones3  42150  sn-axprlem3  42257  sn-exelALT  42258  sn-1ne2  42305  efne0d  42378  remul02  42440  sn-0tie0  42474  pellexlem3  42847  pell1234qrne0  42869  hbtlem6  43146  onsucelab  43281  omabs2  43350  nadd2rabex  43404  or3or  44041  isotone1  44066  isotone2  44067  clsf2  44144  ismnushort  44325  radcnvrat  44338  3impexpbicom  44505  sb5ALT  44550  eexinst01  44551  ax6e2eq  44582  sineq0ALT  44962  tcfr  44985  ssclaxsep  45004  omssaxinf2  45010  fzisoeu  45317  ovnsubaddlem2  46591  ormklocald  46894  natlocalincr  46896  tworepnotupword  46906  funressnfv  47060  faovcl  47217  sprsymrelfo  47489  clnbgrval  47814  cznnring  48183  zlmodzxznm  48419  elbigolo1  48483  dignn0flhalflem1  48541  nn0sumshdig  48549  rrx2xpref1o  48644  fonex  48774  vsetrec  49277