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  2385  equs4  2415  axc15  2421  2ax6elem  2469  dfeumo  2531  mo4  2560  sbcth  3770  sbcth2  3849  ssun3  4145  ssun4  4146  elpreqprlem  4832  uniintsn  4951  sepexlem  5256  axprlem1  5380  axprlem2  5381  axprlem4  5383  axpr  5384  axprlem3OLD  5385  axprlem4OLD  5386  axprlem5OLD  5387  axprOLD  5388  exel  5395  rext  5410  exss  5425  snopeqop  5468  propssopi  5470  uniopel  5478  opthhausdorff  5479  opthhausdorff0  5480  wefrc  5634  relopabi  5787  relop  5816  dmrnssfld  5939  iss  6008  sofld  6162  ordun  6440  funimass2  6601  fvbr0  6889  fvmptg  6968  funsndifnop  7125  ov3  7554  elovmpo  7636  dford5  7762  limsssuc  7828  tfisi  7837  finds1  7877  frxp  8107  frxp2  8125  frxp3  8132  dfrecs3  8343  tfrlem1  8346  oaordi  8512  oaword2  8519  omeulem1  8548  oeworde  8559  oelim2  8561  nnaordi  8584  oaabs2  8615  limenpsi  9121  dif1en  9129  dif1enOLD  9131  enp1iOLD  9231  ordunifi  9243  fidomdm  9291  dffi3  9388  oismo  9499  wdom2d  9539  wdomima2g  9545  epnsym  9568  suc11reg  9578  elom3  9607  cantnfval2  9628  rankunb  9809  rankval4  9826  karden  9854  cardsn  9928  cardlim  9931  cardprclem  9938  fseqdom  9985  dfac12lem3  10105  kmlem2  10111  kmlem10  10119  cflim2  10222  cfslb2n  10227  fin23lem27  10287  fin23lem17  10297  axcc3  10397  axcc4  10398  acncc  10399  domtriomlem  10401  axdclem2  10479  imadomg  10493  alephval2  10531  alephreg  10541  axextnd  10550  fpwwe2lem9  10598  pwfseq  10623  gch2  10634  axgroth3  10790  inaprc  10795  nlt1pi  10865  indpi  10866  1re  11180  mul02lem2  11357  addrid  11360  fimaxre  12133  fiminre  12136  supaddc  12156  supmul1  12158  inelr  12177  rimul  12178  nnge1  12215  zneo  12623  ltweuz  13932  hashrabsn1  14345  hashf1lem2  14427  hash2pwpr  14447  climuni  15524  fsum2d  15743  fsumabs  15773  fsumrlim  15783  fsumo1  15784  fsumiun  15793  fprod2d  15953  efne0d  16069  efne0OLD  16071  ruclem13  16216  dvdslelem  16285  mod2eq1n2dvds  16323  nn0o1gt2  16357  divalglem0  16369  lcmfnnval  16600  prmreclem2  16894  prmreclem3  16895  mreexexd  17615  coaval  18036  xpcco  18150  pltirr  18300  frgpnabllem1  19809  ablfac1eulem  20010  prmgrpsimpgd  20052  mdetunilem9  22513  mretopd  22985  fiuncmp  23297  ptcmpfi  23706  filtop  23748  supnfcls  23913  flimfnfcls  23921  alexsubALTlem2  23941  alexsubALTlem4  23943  trust  24123  rectbntr0  24727  fsumcn  24767  ovoliunlem3  25411  ovolicc2lem4  25427  dyadmax  25505  vitali  25520  itgfsum  25734  dvmptfsum  25885  fta1g  26081  fta1  26222  aannenlem1  26242  aalioulem3  26248  logltb  26515  logdmn0  26555  ang180lem2  26726  angpined  26746  mumullem2  27096  lgsqrmodndvds  27270  gausslemma2dlem0i  27281  2lgs  27324  dchrisum0re  27430  chpdifbnd  27472  pntrlog2bnd  27501  pntibndlem3  27509  pnt3  27529  nofv  27575  nomaxmo  27616  nominmo  27617  noprc  27697  madebday  27817  addsproplem7  27888  negsproplem7  27946  elons2  28165  nbgrval  29269  vtxdginducedm1fi  29478  upgrewlkle2  29540  hiidge0  31033  chsupval  31270  chsupcl  31275  chsupss  31277  ococin  31343  chsupval2  31345  ssjo  31382  h1de2i  31488  pjss2i  31615  pjssmii  31616  sto2i  32172  stge1i  32173  stle0i  32174  stlei  32175  stlesi  32176  stm1i  32178  staddi  32181  stadd3i  32183  golem1  32206  stcltrlem1  32211  mdexchi  32270  chirred  32330  atabsi  32336  abrexdomjm  32442  iocinif  32710  cycpmcl  33079  elrgspnsubrunlem2  33205  voliune  34225  volfiniune  34226  probdif  34417  bnj849  34921  kur14lem9  35201  gonarlem  35381  gonar  35382  goalrlem  35383  goalr  35384  sscoid  35896  limsucncmpi  36428  bj-axc10  36766  bj-alequex  36767  bj-spimtv  36777  bj-moeub  36832  bj-exlimvmpi  36894  bj-exlimmpi  36895  bj-restpw  37075  bj-isrvec  37277  finxpreclem4  37377  domalom  37387  wl-isseteq  37488  wl-embant  37493  wl-orel12  37494  wl-euequf  37557  poimirlem9  37618  abrexdom  37719  heiborlem10  37809  dvrunz  37943  iss2  38321  equcomi1  38888  ax12eq  38929  ax12el  38930  ax12inda  38936  ax12v2-o  38937  cvrnrefN  39270  pmod1i  39837  pmodN  39839  osumcllem11N  39955  pexmidlem8N  39966  pl42lem3N  39970  cdleme18b  40281  dochexmidlem8  41456  imadomfi  41985  sticksstones3  42131  sn-axprlem3  42200  sn-exelALT  42201  sn-1ne2  42248  remul02  42388  sn-0tie0  42434  pellexlem3  42812  pell1234qrne0  42834  hbtlem6  43111  onsucelab  43245  omabs2  43314  nadd2rabex  43368  or3or  44005  isotone1  44030  isotone2  44031  clsf2  44108  ismnushort  44283  radcnvrat  44296  3impexpbicom  44463  sb5ALT  44508  eexinst01  44509  ax6e2eq  44540  sineq0ALT  44919  tcfr  44946  ssclaxsep  44965  omssaxinf2  44971  nregmodel  45000  fzisoeu  45291  ovnsubaddlem2  46562  ormklocald  46865  natlocalincr  46867  tworepnotupword  46877  funressnfv  47034  faovcl  47191  sprsymrelfo  47488  clnbgrval  47813  gpgedgiov  48046  gpgedg2ov  48047  gpgedg2iv  48048  pgnioedg1  48088  pgnioedg2  48089  pgnioedg3  48090  pgnioedg4  48091  pgnioedg5  48092  pgnbgreunbgrlem2lem1  48094  pgnbgreunbgrlem2lem2  48095  pgnbgreunbgrlem2lem3  48096  pgnbgreunbgrlem5lem1  48100  pgnbgreunbgrlem5lem2  48101  cznnring  48240  zlmodzxznm  48476  elbigolo1  48536  dignn0flhalflem1  48594  nn0sumshdig  48602  rrx2xpref1o  48697  fonex  48845  vsetrec  49682