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  1452  merco2  1736  equs4v  2000  alequexv  2001  equcomiv  2014  equcomi  2017  equvinva  2030  aeveq  2057  spimt  2391  equs4  2421  axc15  2427  2ax6elem  2475  dfeumo  2537  mo4  2566  sbcth  3785  sbcth2  3864  ssun3  4160  ssun4  4161  elpreqprlem  4847  uniintsn  4966  sepexlem  5274  axprlem1  5398  axprlem2  5399  axprlem4  5401  axpr  5402  axprlem3OLD  5403  axprlem4OLD  5404  axprlem5OLD  5405  axprOLD  5406  exel  5413  rext  5428  exss  5443  snopeqop  5486  propssopi  5488  uniopel  5496  opthhausdorff  5497  opthhausdorff0  5498  wefrc  5653  relopabi  5806  relop  5835  dmrnssfld  5958  iss  6027  sofld  6181  ordun  6463  funimass2  6624  fvbr0  6910  fvmptg  6989  funsndifnop  7146  ov3  7575  elovmpo  7657  dford5  7783  limsssuc  7850  tfisi  7859  finds1  7900  frxp  8130  frxp2  8148  frxp3  8155  wfrlem5OLD  8332  wfrlem16OLD  8343  dfrecs3  8391  dfrecs3OLD  8392  tfrlem1  8395  oaordi  8563  oaword2  8570  omeulem1  8599  oeworde  8610  oelim2  8612  nnaordi  8635  oaabs2  8666  0domgOLD  9120  limenpsi  9171  dif1en  9179  dif1enOLD  9181  enp1iOLD  9291  ordunifi  9303  fidomdm  9351  dffi3  9448  oismo  9559  wdom2d  9599  wdomima2g  9605  epnsym  9628  suc11reg  9638  elom3  9667  cantnfval2  9688  rankunb  9869  rankval4  9886  karden  9914  cardsn  9988  cardlim  9991  cardprclem  9998  fseqdom  10045  dfac12lem3  10165  kmlem2  10171  kmlem10  10179  cflim2  10282  cfslb2n  10287  fin23lem27  10347  fin23lem17  10357  axcc3  10457  axcc4  10458  acncc  10459  domtriomlem  10461  axdclem2  10539  imadomg  10553  alephval2  10591  alephreg  10601  axextnd  10610  fpwwe2lem9  10658  pwfseq  10683  gch2  10694  axgroth3  10850  inaprc  10855  nlt1pi  10925  indpi  10926  1re  11240  mul02lem2  11417  addrid  11420  fimaxre  12191  fiminre  12194  supaddc  12214  supmul1  12216  inelr  12235  rimul  12236  nnge1  12273  zneo  12681  ltweuz  13984  hashrabsn1  14397  hashf1lem2  14479  hash2pwpr  14499  climuni  15573  fsum2d  15792  fsumabs  15822  fsumrlim  15832  fsumo1  15833  fsumiun  15842  fprod2d  16002  efne0d  16118  efne0OLD  16120  ruclem13  16265  dvdslelem  16333  mod2eq1n2dvds  16371  nn0o1gt2  16405  divalglem0  16417  lcmfnnval  16648  prmreclem2  16942  prmreclem3  16943  mreexexd  17665  coaval  18086  xpcco  18200  pltirr  18350  frgpnabllem1  19859  ablfac1eulem  20060  prmgrpsimpgd  20102  mdetunilem9  22563  mretopd  23035  fiuncmp  23347  ptcmpfi  23756  filtop  23798  supnfcls  23963  flimfnfcls  23971  alexsubALTlem2  23991  alexsubALTlem4  23993  trust  24173  rectbntr0  24777  fsumcn  24817  ovoliunlem3  25462  ovolicc2lem4  25478  dyadmax  25556  vitali  25571  itgfsum  25785  dvmptfsum  25936  fta1g  26132  fta1  26273  aannenlem1  26293  aalioulem3  26299  logltb  26566  logdmn0  26606  ang180lem2  26777  angpined  26797  mumullem2  27147  lgsqrmodndvds  27321  gausslemma2dlem0i  27332  2lgs  27375  dchrisum0re  27481  chpdifbnd  27523  pntrlog2bnd  27552  pntibndlem3  27560  pnt3  27580  nofv  27626  nomaxmo  27667  nominmo  27668  noprc  27748  madebday  27868  addsproplem7  27939  negsproplem7  27997  elons2  28216  nbgrval  29320  vtxdginducedm1fi  29529  upgrewlkle2  29591  hiidge0  31084  chsupval  31321  chsupcl  31326  chsupss  31328  ococin  31394  chsupval2  31396  ssjo  31433  h1de2i  31539  pjss2i  31666  pjssmii  31667  sto2i  32223  stge1i  32224  stle0i  32225  stlei  32226  stlesi  32227  stm1i  32229  staddi  32232  stadd3i  32234  golem1  32257  stcltrlem1  32262  mdexchi  32321  chirred  32381  atabsi  32387  abrexdomjm  32493  iocinif  32763  cycpmcl  33132  elrgspnsubrunlem2  33248  voliune  34265  volfiniune  34266  probdif  34457  bnj849  34961  kur14lem9  35241  gonarlem  35421  gonar  35422  goalrlem  35423  goalr  35424  sscoid  35936  limsucncmpi  36468  bj-axc10  36806  bj-alequex  36807  bj-spimtv  36817  bj-moeub  36872  bj-exlimvmpi  36934  bj-exlimmpi  36935  bj-restpw  37115  bj-isrvec  37317  finxpreclem4  37417  domalom  37427  wl-isseteq  37528  wl-embant  37533  wl-orel12  37534  wl-euequf  37597  poimirlem9  37658  abrexdom  37759  heiborlem10  37849  dvrunz  37983  iss2  38367  equcomi1  38923  ax12eq  38964  ax12el  38965  ax12inda  38971  ax12v2-o  38972  cvrnrefN  39305  pmod1i  39872  pmodN  39874  osumcllem11N  39990  pexmidlem8N  40001  pl42lem3N  40005  cdleme18b  40316  dochexmidlem8  41491  imadomfi  42020  sticksstones3  42166  sn-axprlem3  42235  sn-exelALT  42236  sn-1ne2  42283  remul02  42423  sn-0tie0  42457  pellexlem3  42829  pell1234qrne0  42851  hbtlem6  43128  onsucelab  43262  omabs2  43331  nadd2rabex  43385  or3or  44022  isotone1  44047  isotone2  44048  clsf2  44125  ismnushort  44300  radcnvrat  44313  3impexpbicom  44480  sb5ALT  44525  eexinst01  44526  ax6e2eq  44557  sineq0ALT  44936  tcfr  44963  ssclaxsep  44982  omssaxinf2  44988  nregmodel  45017  fzisoeu  45309  ovnsubaddlem2  46580  ormklocald  46883  natlocalincr  46885  tworepnotupword  46895  funressnfv  47052  faovcl  47209  sprsymrelfo  47491  clnbgrval  47816  cznnring  48217  zlmodzxznm  48453  elbigolo1  48517  dignn0flhalflem1  48575  nn0sumshdig  48583  rrx2xpref1o  48678  fonex  48822  vsetrec  49547