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  699  mp3an3  1453  merco2  1738  equs4v  2002  alequexv  2003  equcomiv  2016  equcomi  2019  equvinva  2032  aeveq  2060  spimt  2391  equs4  2421  axc15  2427  2ax6elem  2475  dfeumo  2537  mo4  2567  sbcth  3744  sbcth2  3823  ssun3  4121  ssun4  4122  elpreqprlem  4810  uniintsn  4928  sepexlem  5234  axprlem2  5359  axprlem4  5361  axpr  5362  axprlem1OLD  5363  axprlem3OLD  5364  axprlem4OLD  5365  axprlem5OLD  5366  axprOLD  5367  axprglem  5371  exel  5379  rext  5393  exss  5408  snopeqop  5452  propssopi  5454  uniopel  5462  opthhausdorff  5463  opthhausdorff0  5464  wefrc  5616  relopabi  5769  relop  5797  dmrnssfld  5921  iss  5992  sofld  6143  ordun  6421  funimass2  6573  fvbr0  6859  fvmptg  6937  funsndifnop  7096  ov3  7521  elovmpo  7603  dford5  7729  limsssuc  7792  tfisi  7801  finds1  7841  frxp  8067  frxp2  8085  frxp3  8092  dfrecs3  8303  tfrlem1  8306  oaordi  8472  oaword2  8479  omeulem1  8508  oeworde  8520  oelim2  8522  nnaordi  8545  oaabs2  8576  limenpsi  9081  dif1en  9087  ordunifi  9191  fidomdm  9235  dffi3  9335  oismo  9446  wdom2d  9486  wdomima2g  9492  epnsym  9519  suc11reg  9529  elom3  9558  cantnfval2  9579  rankunb  9763  rankval4  9780  karden  9808  cardsn  9882  cardlim  9885  cardprclem  9892  fseqdom  9937  dfac12lem3  10057  kmlem2  10063  kmlem10  10071  cflim2  10174  cfslb2n  10179  fin23lem27  10239  fin23lem17  10249  axcc3  10349  axcc4  10350  acncc  10351  domtriomlem  10353  axdclem2  10431  imadomg  10445  alephval2  10484  alephreg  10494  axextnd  10503  fpwwe2lem9  10551  pwfseq  10576  gch2  10587  axgroth3  10743  inaprc  10748  nlt1pi  10818  indpi  10819  1re  11133  mul02lem2  11311  addrid  11314  fimaxre  12087  fiminre  12090  supaddc  12110  supmul1  12112  rimul  12137  nnge1  12174  zneo  12576  ltweuz  13885  hashrabsn1  14298  hashf1lem2  14380  hash2pwpr  14400  climuni  15476  fsum2d  15695  fsumabs  15725  fsumrlim  15735  fsumo1  15736  fsumiun  15745  fprod2d  15905  efne0d  16021  efne0OLD  16023  ruclem13  16168  dvdslelem  16237  mod2eq1n2dvds  16275  nn0o1gt2  16309  divalglem0  16321  lcmfnnval  16552  prmreclem2  16846  prmreclem3  16847  mreexexd  17572  coaval  17993  xpcco  18107  pltirr  18257  frgpnabllem1  19806  ablfac1eulem  20007  prmgrpsimpgd  20049  mdetunilem9  22563  mretopd  23035  fiuncmp  23347  ptcmpfi  23756  filtop  23798  supnfcls  23963  flimfnfcls  23971  alexsubALTlem2  23991  alexsubALTlem4  23993  trust  24172  rectbntr0  24776  fsumcn  24815  ovoliunlem3  25449  ovolicc2lem4  25465  dyadmax  25543  vitali  25558  itgfsum  25772  dvmptfsum  25920  fta1g  26116  fta1  26256  aannenlem1  26276  aalioulem3  26282  logltb  26549  logdmn0  26589  ang180lem2  26760  angpined  26780  mumullem2  27130  lgsqrmodndvds  27304  gausslemma2dlem0i  27315  2lgs  27358  dchrisum0re  27464  chpdifbnd  27506  pntrlog2bnd  27535  pntibndlem3  27543  pnt3  27563  nofv  27609  nomaxmo  27650  nominmo  27651  noprc  27736  madebday  27880  addsproplem7  27955  negsproplem7  28014  elons2  28238  nbgrval  29393  vtxdginducedm1fi  29602  upgrewlkle2  29664  hiidge0  31158  chsupval  31395  chsupcl  31400  chsupss  31402  ococin  31468  chsupval2  31470  ssjo  31507  h1de2i  31613  pjss2i  31740  pjssmii  31741  sto2i  32297  stge1i  32298  stle0i  32299  stlei  32300  stlesi  32301  stm1i  32303  staddi  32306  stadd3i  32308  golem1  32331  stcltrlem1  32336  mdexchi  32395  chirred  32455  atabsi  32461  abrexdomjm  32566  iocinif  32844  cycpmcl  33182  elrgspnsubrunlem2  33314  voliune  34379  volfiniune  34380  probdif  34570  bnj849  35073  axprALT2  35259  onvf1odlem4  35294  onvf1od  35295  kur14lem9  35402  gonarlem  35582  gonar  35583  goalrlem  35584  goalr  35585  sscoid  36099  limsucncmpi  36633  axtco1from2  36663  axtcond  36666  bj-nnf-spime  37070  bj-axc10  37088  bj-alequex  37089  bj-spimtv  37099  bj-moeub  37154  bj-exlimvmpi  37216  bj-exlimmpi  37217  bj-restpw  37402  bj-isrvec  37606  finxpreclem4  37706  domalom  37716  wl-isseteq  37817  wl-embant  37826  wl-orel12  37827  wl-euequf  37890  poimirlem9  37941  abrexdom  38042  heiborlem10  38132  dvrunz  38266  iss2  38656  equcomi1  39337  ax12eq  39378  ax12el  39379  ax12inda  39385  ax12v2-o  39386  cvrnrefN  39719  pmod1i  40285  pmodN  40287  osumcllem11N  40403  pexmidlem8N  40414  pl42lem3N  40418  cdleme18b  40729  dochexmidlem8  41904  imadomfi  42433  sticksstones3  42579  sn-axprlem3  42651  sn-exelALT  42652  sn-1ne2  42696  remul02  42836  sn-0tie0  42895  pellexlem3  43262  pell1234qrne0  43284  hbtlem6  43560  onsucelab  43694  omabs2  43763  nadd2rabex  43817  or3or  44453  isotone1  44478  isotone2  44479  clsf2  44556  ismnushort  44731  radcnvrat  44744  3impexpbicom  44910  sb5ALT  44955  eexinst01  44956  ax6e2eq  44987  sineq0ALT  45366  tcfr  45393  ssclaxsep  45412  omssaxinf2  45418  nregmodel  45447  fzisoeu  45736  ovnsubaddlem2  47003  ormklocald  47306  natlocalincr  47308  tannpoly  47324  funressnfv  47477  faovcl  47634  sprsymrelfo  47931  clnbgrval  48256  gpgedgiov  48499  gpgedg2ov  48500  gpgedg2iv  48501  pgnioedg1  48542  pgnioedg2  48543  pgnioedg3  48544  pgnioedg4  48545  pgnioedg5  48546  pgnbgreunbgrlem2lem1  48548  pgnbgreunbgrlem2lem2  48549  pgnbgreunbgrlem2lem3  48550  pgnbgreunbgrlem5lem1  48554  pgnbgreunbgrlem5lem2  48555  cznnring  48696  zlmodzxznm  48931  elbigolo1  48991  dignn0flhalflem1  49049  nn0sumshdig  49057  rrx2xpref1o  49152  fonex  49300  vsetrec  50136