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  708  mp3an3  1471  merco2  1756  equs4v  2020  alequexv  2021  equcomiv  2034  equcomi  2037  equvinva  2050  aeveq  2078  spimt  2417  equs4  2447  axc15  2453  2ax6elem  2501  dfeumo  2563  mo4  2593  sbcth  3759  sbcth2  3837  ssun3  4132  ssun4  4133  elpreqprlem  4824  uniintsn  4943  sepexlem  5249  axprlem2  5381  axprlem4  5383  axpr  5384  axprlem1OLD  5385  axprlem3OLD  5386  axprlem4OLD  5387  axprlem5OLD  5388  axprOLD  5389  axprglem  5393  exel  5401  rext  5415  exss  5430  snopeqop  5475  propssopi  5477  uniopel  5485  opthhausdorff  5486  opthhausdorff0  5487  wefrc  5641  relopabi  5795  relop  5822  dmrnssfld  5950  iss  6024  sofld  6173  ordun  6452  funimass2  6604  fvbr0  6894  fvmptg  6973  funsndifnop  7134  ov3  7559  elovmpo  7641  dford5  7767  limsssuc  7830  tfisi  7839  finds1  7880  frxp  8106  frxp2  8124  frxp3  8131  dfrecs3  8343  tfrlem1  8346  oaordi  8515  oaword2  8522  omeulem1  8551  oeworde  8563  oelim2  8565  nnaordi  8588  oaabs2  8619  limenpsi  9124  dif1en  9130  ordunifi  9234  fidomdm  9277  dffi3  9377  oismo  9488  wdom2d  9528  wdomima2g  9534  epnsym  9564  suc11reg  9574  elom3  9603  cantnfval2  9624  rankunb  9808  rankval4  9825  karden  9853  cardsn  9927  cardlim  9930  cardprclem  9937  fseqdom  9982  dfac12lem3  10102  kmlem2  10108  kmlem10  10116  cflim2  10220  cfslb2n  10225  fin23lem27  10285  fin23lem17  10295  axcc3  10395  axcc4  10396  acncc  10397  domtriomlem  10399  axdclem2  10477  imadomg  10491  alephval2  10530  alephreg  10540  axextnd  10549  fpwwe2lem9  10597  pwfseq  10622  gch2  10633  axgroth3  10789  inaprc  10794  nlt1pi  10864  indpi  10865  1re  11181  mul02lem2  11360  addrid  11363  fimaxre  12136  fiminre  12139  supaddc  12159  supmul1  12161  rimul  12186  nnge1  12241  zneo  12656  ltweuz  13974  hashrabsn1  14387  hashf1lem2  14469  hash2pwpr  14489  climuni  15579  fsum2d  15798  fsumabs  15829  fsumrlim  15839  fsumo1  15840  fsumiun  15849  fprod2d  16011  efne0d  16127  efne0OLD  16129  ruclem13  16274  dvdslelem  16343  mod2eq1n2dvds  16381  nn0o1gt2  16415  divalglem0  16427  lcmfnnval  16658  prmreclem2  16953  prmreclem3  16954  mreexexd  17680  coaval  18101  xpcco  18215  pltirr  18365  frgpnabllem1  19913  ablfac1eulem  20114  prmgrpsimpgd  20156  mdetunilem9  22680  mretopd  23152  fiuncmp  23464  ptcmpfi  23873  filtop  23915  supnfcls  24080  flimfnfcls  24088  alexsubALTlem2  24108  alexsubALTlem4  24110  trust  24289  rectbntr0  24893  fsumcn  24932  ovoliunlem3  25566  ovolicc2lem4  25582  dyadmax  25660  vitali  25675  itgfsum  25889  dvmptfsum  26037  fta1g  26230  fta1  26372  aannenlem1  26392  aalioulem3  26398  logltb  26665  logdmn0  26705  ang180lem2  26875  angpined  26895  mumullem2  27244  lgsqrmodndvds  27417  gausslemma2dlem0i  27428  2lgs  27471  dchrisum0re  27577  chpdifbnd  27619  pntrlog2bnd  27648  pntibndlem3  27656  pnt3  27676  nofv  27721  nomaxmo  27762  nominmo  27763  noprc  27849  madebday  27993  addsproplem7  28068  negsproplem7  28127  elons2  28351  nbgrval  29537  vtxdginducedm1fi  29745  upgrewlkle2  29807  hiidge0  31301  chsupval  31538  chsupcl  31543  chsupss  31545  ococin  31611  chsupval2  31613  ssjo  31650  h1de2i  31756  pjss2i  31883  pjssmii  31884  sto2i  32440  stge1i  32441  stle0i  32442  stlei  32443  stlesi  32444  stm1i  32446  staddi  32449  stadd3i  32451  golem1  32474  stcltrlem1  32479  mdexchi  32538  chirred  32598  atabsi  32604  abrexdomjm  32706  iocinif  32983  cycpmcl  33296  elrgspnsubrunlem2  33429  voliune  34526  volfiniune  34527  probdif  34717  bnj849  35220  axprALT2  35405  onvf1odlem4  35449  onvf1od  35450  onvfowev  35459  kur14lem9  35564  gonarlem  35744  gonar  35745  goalrlem  35746  goalr  35747  sscoid  36261  limsucncmpi  36805  axtco1from2  36835  axtcond  36838  bj-nnf-spime  37250  bj-axc10  37268  bj-alequex  37269  bj-spimtv  37279  bj-moeub  37334  bj-exlimvmpi  37396  bj-exlimmpi  37397  bj-restpw  37582  bj-isrvec  37786  finxpreclem4  37888  domalom  37898  wl-isseteq  37999  wl-embant  38013  wl-orel12  38014  wl-euequf  38077  poimirlem9  38128  abrexdom  38229  heiborlem10  38319  dvrunz  38453  iss2  38843  equcomi1  39524  ax12eq  39565  ax12el  39566  ax12inda  39572  ax12v2-o  39573  cvrnrefN  39906  pmod1i  40472  pmodN  40474  osumcllem11N  40590  pexmidlem8N  40601  pl42lem3N  40605  cdleme18b  40916  dochexmidlem8  42091  imadomfi  42619  sticksstones3  42765  sn-axprlem3  42837  sn-exelALT  42838  sn-1ne2  42880  remul02  43014  sn-0tie0  43073  pellexlem3  43408  pell1234qrne0  43430  hbtlem6  43706  onsucelab  43840  omabs2  43909  nadd2rabex  43963  or3or  44599  isotone1  44624  isotone2  44625  clsf2  44702  ismnushort  44877  radcnvrat  44890  3impexpbicom  45056  sb5ALT  45101  eexinst01  45102  ax6e2eq  45133  sineq0ALT  45512  tcfr  45539  ssclaxsep  45558  omssaxinf2  45564  nregmodel  45593  fzisoeu  45879  ovnsubaddlem2  47145  ormklocald  47450  natlocalincr  47452  tannpoly  47484  funressnfv  47637  faovcl  47794  sprsymrelfo  48103  clnbgrval  48444  gpgedgiov  48687  gpgedg2ov  48688  gpgedg2iv  48689  pgnioedg1  48730  pgnioedg2  48731  pgnioedg3  48732  pgnioedg4  48733  pgnioedg5  48734  pgnbgreunbgrlem2lem1  48736  pgnbgreunbgrlem2lem2  48737  pgnbgreunbgrlem2lem3  48738  pgnbgreunbgrlem5lem1  48742  pgnbgreunbgrlem5lem2  48743  cznnring  48884  zlmodzxznm  49119  elbigolo1  49179  dignn0flhalflem1  49237  nn0sumshdig  49245  rrx2xpref1o  49340  fonex  49488  vsetrec  50324