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  3655  sbcth  3791  sbcth2  3877  ssun3  4173  ssun4  4174  elpreqprlem  4865  uniintsn  4990  axprlem1  5420  axprlem2  5421  axprlem3  5422  axprlem4  5423  axprlem5  5424  axpr  5425  exel  5432  rext  5447  exss  5462  snopeqop  5505  propssopi  5507  uniopel  5515  opthhausdorff  5516  opthhausdorff0  5517  wefrc  5669  relopabi  5820  relop  5848  dmrnssfld  5967  iss  6033  sofld  6183  ordun  6465  funimass2  6628  fvbr0  6917  fvmptg  6992  funsndifnop  7144  ov3  7565  elovmpo  7646  dford5  7766  limsssuc  7834  tfisi  7843  finds1  7887  frxp  8107  frxp2  8125  frxp3  8132  wfrlem5OLD  8308  wfrlem16OLD  8319  dfrecs3  8367  dfrecs3OLD  8368  tfrlem1  8371  oaordi  8542  oaword2  8549  omeulem1  8578  oeworde  8589  oelim2  8591  nnaordi  8614  oaabs2  8644  0domgOLD  9097  limenpsi  9148  dif1en  9156  dif1enOLD  9158  enp1iOLD  9276  findcard2OLD  9280  ordunifi  9289  fidomdm  9325  dffi3  9422  oismo  9531  wdom2d  9571  wdomima2g  9577  epnsym  9600  suc11reg  9610  elom3  9639  cantnfval2  9660  rankunb  9841  rankval4  9858  karden  9886  cardsn  9960  cardlim  9963  cardprclem  9970  fseqdom  10017  dfac12lem3  10136  kmlem2  10142  kmlem10  10150  cflim2  10254  cfslb2n  10259  fin23lem27  10319  fin23lem17  10329  axcc3  10429  axcc4  10430  acncc  10431  domtriomlem  10433  axdclem2  10511  imadomg  10525  alephval2  10563  alephreg  10573  axextnd  10582  fpwwe2lem9  10630  pwfseq  10655  gch2  10666  axgroth3  10822  inaprc  10827  nlt1pi  10897  indpi  10898  1re  11210  mul02lem2  11387  addrid  11390  fimaxre  12154  fiminre  12157  supaddc  12177  supmul1  12179  inelr  12198  rimul  12199  nnge1  12236  zneo  12641  ltweuz  13922  hashrabsn1  14330  hashf1lem2  14413  hash2pwpr  14433  climuni  15492  fsum2d  15713  fsumabs  15743  fsumrlim  15753  fsumo1  15754  fsumiun  15763  fprod2d  15921  efne0  16036  ruclem13  16181  dvdslelem  16248  mod2eq1n2dvds  16286  nn0o1gt2  16320  divalglem0  16332  lcmfnnval  16557  prmreclem2  16846  prmreclem3  16847  mreexexd  17588  coaval  18014  xpcco  18131  pltirr  18284  frgpnabllem1  19733  ablfac1eulem  19934  prmgrpsimpgd  19976  mdetunilem9  22104  mretopd  22578  fiuncmp  22890  ptcmpfi  23299  filtop  23341  supnfcls  23506  flimfnfcls  23514  alexsubALTlem2  23534  alexsubALTlem4  23536  trust  23716  rectbntr0  24330  fsumcn  24368  ovoliunlem3  25003  ovolicc2lem4  25019  dyadmax  25097  vitali  25112  itgfsum  25326  dvmptfsum  25474  fta1g  25667  fta1  25803  aannenlem1  25823  aalioulem3  25829  logltb  26090  logdmn0  26130  ang180lem2  26295  angpined  26315  mumullem2  26664  lgsqrmodndvds  26836  gausslemma2dlem0i  26847  2lgs  26890  dchrisum0re  26996  chpdifbnd  27038  pntrlog2bnd  27067  pntibndlem3  27075  pnt3  27095  nofv  27140  nomaxmo  27181  nominmo  27182  noprc  27261  madebday  27374  addsproplem7  27439  negsproplem7  27488  nbgrval  28573  vtxdginducedm1fi  28781  upgrewlkle2  28843  hiidge0  30329  chsupval  30566  chsupcl  30571  chsupss  30573  ococin  30639  chsupval2  30641  ssjo  30678  h1de2i  30784  pjss2i  30911  pjssmii  30912  sto2i  31468  stge1i  31469  stle0i  31470  stlei  31471  stlesi  31472  stm1i  31474  staddi  31477  stadd3i  31479  golem1  31502  stcltrlem1  31507  mdexchi  31566  chirred  31626  atabsi  31632  abrexdomjm  31722  iocinif  31970  cycpmcl  32253  voliune  33165  volfiniune  33166  probdif  33357  bnj849  33874  kur14lem9  34143  gonarlem  34323  gonar  34324  goalrlem  34325  goalr  34326  sscoid  34823  limsucncmpi  35268  bj-axc10  35599  bj-alequex  35600  bj-spimtv  35610  bj-moeub  35666  bj-exlimvmpi  35729  bj-exlimmpi  35730  bj-restpw  35911  bj-isrvec  36113  finxpreclem4  36213  domalom  36223  wl-embant  36317  wl-orel12  36318  wl-euequf  36377  poimirlem9  36435  abrexdom  36536  heiborlem10  36626  dvrunz  36760  iss2  37151  equcomi1  37708  ax12eq  37749  ax12el  37750  ax12inda  37756  ax12v2-o  37757  cvrnrefN  38090  pmod1i  38657  pmodN  38659  osumcllem11N  38775  pexmidlem8N  38786  pl42lem3N  38790  cdleme18b  39101  dochexmidlem8  40276  sticksstones3  40902  sn-axprlem3  40982  sn-exelALT  40983  sn-1ne2  41129  remul02  41222  sn-0tie0  41256  pellexlem3  41502  pell1234qrne0  41524  hbtlem6  41804  onsucelab  41946  omabs2  42015  nadd2rabex  42069  or3or  42707  isotone1  42732  isotone2  42733  clsf2  42810  ismnushort  42993  radcnvrat  43006  3impexpbicom  43173  sb5ALT  43219  eexinst01  43220  ax6e2eq  43251  sineq0ALT  43631  fzisoeu  43945  ovnsubaddlem2  45222  natlocalincr  45525  tworepnotupword  45535  funressnfv  45688  faovcl  45843  sprsymrelfo  46100  cznnring  46756  zlmodzxznm  47080  elbigolo1  47145  dignn0flhalflem1  47203  nn0sumshdig  47211  rrx2xpref1o  47306  vsetrec  47650