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  697  mp3an3  1451  merco2  1739  equs4v  2004  alequexv  2005  equcomiv  2018  equcomi  2021  equvinva  2034  aeveq  2060  spimt  2386  equs4  2416  axc15  2422  2ax6elem  2470  dfeumo  2532  mo4  2561  pm13.183  3657  sbcth  3793  sbcth2  3879  ssun3  4175  ssun4  4176  elpreqprlem  4867  uniintsn  4992  axprlem1  5422  axprlem2  5423  axprlem3  5424  axprlem4  5425  axprlem5  5426  axpr  5427  exel  5434  rext  5449  exss  5464  snopeqop  5507  propssopi  5509  uniopel  5517  opthhausdorff  5518  opthhausdorff0  5519  wefrc  5671  relopabi  5823  relop  5851  dmrnssfld  5970  iss  6036  sofld  6187  ordun  6469  funimass2  6632  fvbr0  6921  fvmptg  6997  funsndifnop  7149  ov3  7570  elovmpo  7651  dford5  7771  limsssuc  7839  tfisi  7848  finds1  7892  frxp  8112  frxp2  8130  frxp3  8137  wfrlem5OLD  8313  wfrlem16OLD  8324  dfrecs3  8372  dfrecs3OLD  8373  tfrlem1  8376  oaordi  8546  oaword2  8553  omeulem1  8582  oeworde  8593  oelim2  8595  nnaordi  8618  oaabs2  8648  0domgOLD  9101  limenpsi  9152  dif1en  9160  dif1enOLD  9162  enp1iOLD  9280  findcard2OLD  9284  ordunifi  9293  fidomdm  9329  dffi3  9426  oismo  9535  wdom2d  9575  wdomima2g  9581  epnsym  9604  suc11reg  9614  elom3  9643  cantnfval2  9664  rankunb  9845  rankval4  9862  karden  9890  cardsn  9964  cardlim  9967  cardprclem  9974  fseqdom  10021  dfac12lem3  10140  kmlem2  10146  kmlem10  10154  cflim2  10258  cfslb2n  10263  fin23lem27  10323  fin23lem17  10333  axcc3  10433  axcc4  10434  acncc  10435  domtriomlem  10437  axdclem2  10515  imadomg  10529  alephval2  10567  alephreg  10577  axextnd  10586  fpwwe2lem9  10634  pwfseq  10659  gch2  10670  axgroth3  10826  inaprc  10831  nlt1pi  10901  indpi  10902  1re  11214  mul02lem2  11391  addrid  11394  fimaxre  12158  fiminre  12161  supaddc  12181  supmul1  12183  inelr  12202  rimul  12203  nnge1  12240  zneo  12645  ltweuz  13926  hashrabsn1  14334  hashf1lem2  14417  hash2pwpr  14437  climuni  15496  fsum2d  15717  fsumabs  15747  fsumrlim  15757  fsumo1  15758  fsumiun  15767  fprod2d  15925  efne0  16040  ruclem13  16185  dvdslelem  16252  mod2eq1n2dvds  16290  nn0o1gt2  16324  divalglem0  16336  lcmfnnval  16561  prmreclem2  16850  prmreclem3  16851  mreexexd  17592  coaval  18018  xpcco  18135  pltirr  18288  frgpnabllem1  19741  ablfac1eulem  19942  prmgrpsimpgd  19984  mdetunilem9  22122  mretopd  22596  fiuncmp  22908  ptcmpfi  23317  filtop  23359  supnfcls  23524  flimfnfcls  23532  alexsubALTlem2  23552  alexsubALTlem4  23554  trust  23734  rectbntr0  24348  fsumcn  24386  ovoliunlem3  25021  ovolicc2lem4  25037  dyadmax  25115  vitali  25130  itgfsum  25344  dvmptfsum  25492  fta1g  25685  fta1  25821  aannenlem1  25841  aalioulem3  25847  logltb  26108  logdmn0  26148  ang180lem2  26315  angpined  26335  mumullem2  26684  lgsqrmodndvds  26856  gausslemma2dlem0i  26867  2lgs  26910  dchrisum0re  27016  chpdifbnd  27058  pntrlog2bnd  27087  pntibndlem3  27095  pnt3  27115  nofv  27160  nomaxmo  27201  nominmo  27202  noprc  27281  madebday  27394  addsproplem7  27459  negsproplem7  27508  nbgrval  28593  vtxdginducedm1fi  28801  upgrewlkle2  28863  hiidge0  30351  chsupval  30588  chsupcl  30593  chsupss  30595  ococin  30661  chsupval2  30663  ssjo  30700  h1de2i  30806  pjss2i  30933  pjssmii  30934  sto2i  31490  stge1i  31491  stle0i  31492  stlei  31493  stlesi  31494  stm1i  31496  staddi  31499  stadd3i  31501  golem1  31524  stcltrlem1  31529  mdexchi  31588  chirred  31648  atabsi  31654  abrexdomjm  31744  iocinif  31992  cycpmcl  32275  voliune  33227  volfiniune  33228  probdif  33419  bnj849  33936  kur14lem9  34205  gonarlem  34385  gonar  34386  goalrlem  34387  goalr  34388  sscoid  34885  limsucncmpi  35330  bj-axc10  35661  bj-alequex  35662  bj-spimtv  35672  bj-moeub  35728  bj-exlimvmpi  35791  bj-exlimmpi  35792  bj-restpw  35973  bj-isrvec  36175  finxpreclem4  36275  domalom  36285  wl-embant  36379  wl-orel12  36380  wl-euequf  36439  poimirlem9  36497  abrexdom  36598  heiborlem10  36688  dvrunz  36822  iss2  37213  equcomi1  37770  ax12eq  37811  ax12el  37812  ax12inda  37818  ax12v2-o  37819  cvrnrefN  38152  pmod1i  38719  pmodN  38721  osumcllem11N  38837  pexmidlem8N  38848  pl42lem3N  38852  cdleme18b  39163  dochexmidlem8  40338  sticksstones3  40964  sn-axprlem3  41034  sn-exelALT  41035  sn-1ne2  41179  remul02  41278  sn-0tie0  41312  pellexlem3  41569  pell1234qrne0  41591  hbtlem6  41871  onsucelab  42013  omabs2  42082  nadd2rabex  42136  or3or  42774  isotone1  42799  isotone2  42800  clsf2  42877  ismnushort  43060  radcnvrat  43073  3impexpbicom  43240  sb5ALT  43286  eexinst01  43287  ax6e2eq  43318  sineq0ALT  43698  fzisoeu  44010  ovnsubaddlem2  45287  natlocalincr  45590  tworepnotupword  45600  funressnfv  45753  faovcl  45908  sprsymrelfo  46165  cznnring  46854  zlmodzxznm  47178  elbigolo1  47243  dignn0flhalflem1  47301  nn0sumshdig  47309  rrx2xpref1o  47404  vsetrec  47748