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  1737  equs4v  2001  alequexv  2002  equcomiv  2015  equcomi  2018  equvinva  2031  aeveq  2059  spimt  2386  equs4  2416  axc15  2422  2ax6elem  2470  dfeumo  2532  mo4  2561  sbcth  3751  sbcth2  3830  ssun3  4127  ssun4  4128  elpreqprlem  4815  uniintsn  4933  sepexlem  5235  axprlem1  5359  axprlem2  5360  axprlem4  5362  axpr  5363  axprlem3OLD  5364  axprlem4OLD  5365  axprlem5OLD  5366  axprOLD  5367  exel  5374  rext  5387  exss  5401  snopeqop  5444  propssopi  5446  uniopel  5454  opthhausdorff  5455  opthhausdorff0  5456  wefrc  5608  relopabi  5761  relop  5789  dmrnssfld  5912  iss  5983  sofld  6134  ordun  6412  funimass2  6564  fvbr0  6849  fvmptg  6927  funsndifnop  7084  ov3  7509  elovmpo  7591  dford5  7717  limsssuc  7780  tfisi  7789  finds1  7829  frxp  8056  frxp2  8074  frxp3  8081  dfrecs3  8292  tfrlem1  8295  oaordi  8461  oaword2  8468  omeulem1  8497  oeworde  8508  oelim2  8510  nnaordi  8533  oaabs2  8564  limenpsi  9065  dif1en  9071  ordunifi  9174  fidomdm  9218  dffi3  9315  oismo  9426  wdom2d  9466  wdomima2g  9472  epnsym  9499  suc11reg  9509  elom3  9538  cantnfval2  9559  rankunb  9743  rankval4  9760  karden  9788  cardsn  9862  cardlim  9865  cardprclem  9872  fseqdom  9917  dfac12lem3  10037  kmlem2  10043  kmlem10  10051  cflim2  10154  cfslb2n  10159  fin23lem27  10219  fin23lem17  10229  axcc3  10329  axcc4  10330  acncc  10331  domtriomlem  10333  axdclem2  10411  imadomg  10425  alephval2  10463  alephreg  10473  axextnd  10482  fpwwe2lem9  10530  pwfseq  10555  gch2  10566  axgroth3  10722  inaprc  10727  nlt1pi  10797  indpi  10798  1re  11112  mul02lem2  11290  addrid  11293  fimaxre  12066  fiminre  12069  supaddc  12089  supmul1  12091  rimul  12116  nnge1  12153  zneo  12556  ltweuz  13868  hashrabsn1  14281  hashf1lem2  14363  hash2pwpr  14383  climuni  15459  fsum2d  15678  fsumabs  15708  fsumrlim  15718  fsumo1  15719  fsumiun  15728  fprod2d  15888  efne0d  16004  efne0OLD  16006  ruclem13  16151  dvdslelem  16220  mod2eq1n2dvds  16258  nn0o1gt2  16292  divalglem0  16304  lcmfnnval  16535  prmreclem2  16829  prmreclem3  16830  mreexexd  17554  coaval  17975  xpcco  18089  pltirr  18239  frgpnabllem1  19785  ablfac1eulem  19986  prmgrpsimpgd  20028  mdetunilem9  22535  mretopd  23007  fiuncmp  23319  ptcmpfi  23728  filtop  23770  supnfcls  23935  flimfnfcls  23943  alexsubALTlem2  23963  alexsubALTlem4  23965  trust  24144  rectbntr0  24748  fsumcn  24788  ovoliunlem3  25432  ovolicc2lem4  25448  dyadmax  25526  vitali  25541  itgfsum  25755  dvmptfsum  25906  fta1g  26102  fta1  26243  aannenlem1  26263  aalioulem3  26269  logltb  26536  logdmn0  26576  ang180lem2  26747  angpined  26767  mumullem2  27117  lgsqrmodndvds  27291  gausslemma2dlem0i  27302  2lgs  27345  dchrisum0re  27451  chpdifbnd  27493  pntrlog2bnd  27522  pntibndlem3  27530  pnt3  27550  nofv  27596  nomaxmo  27637  nominmo  27638  noprc  27719  madebday  27845  addsproplem7  27918  negsproplem7  27976  elons2  28195  nbgrval  29314  vtxdginducedm1fi  29523  upgrewlkle2  29585  hiidge0  31078  chsupval  31315  chsupcl  31320  chsupss  31322  ococin  31388  chsupval2  31390  ssjo  31427  h1de2i  31533  pjss2i  31660  pjssmii  31661  sto2i  32217  stge1i  32218  stle0i  32219  stlei  32220  stlesi  32221  stm1i  32223  staddi  32226  stadd3i  32228  golem1  32251  stcltrlem1  32256  mdexchi  32315  chirred  32375  atabsi  32381  abrexdomjm  32487  iocinif  32764  cycpmcl  33085  elrgspnsubrunlem2  33215  voliune  34242  volfiniune  34243  probdif  34433  bnj849  34937  onvf1odlem4  35150  onvf1od  35151  kur14lem9  35258  gonarlem  35438  gonar  35439  goalrlem  35440  goalr  35441  sscoid  35955  limsucncmpi  36489  bj-axc10  36827  bj-alequex  36828  bj-spimtv  36838  bj-moeub  36893  bj-exlimvmpi  36955  bj-exlimmpi  36956  bj-restpw  37136  bj-isrvec  37338  finxpreclem4  37438  domalom  37448  wl-isseteq  37549  wl-embant  37554  wl-orel12  37555  wl-euequf  37618  poimirlem9  37679  abrexdom  37780  heiborlem10  37870  dvrunz  38004  iss2  38386  equcomi1  39009  ax12eq  39050  ax12el  39051  ax12inda  39057  ax12v2-o  39058  cvrnrefN  39391  pmod1i  39957  pmodN  39959  osumcllem11N  40075  pexmidlem8N  40086  pl42lem3N  40090  cdleme18b  40401  dochexmidlem8  41576  imadomfi  42105  sticksstones3  42251  sn-axprlem3  42320  sn-exelALT  42321  sn-1ne2  42368  remul02  42508  sn-0tie0  42554  pellexlem3  42934  pell1234qrne0  42956  hbtlem6  43232  onsucelab  43366  omabs2  43435  nadd2rabex  43489  or3or  44126  isotone1  44151  isotone2  44152  clsf2  44229  ismnushort  44404  radcnvrat  44417  3impexpbicom  44583  sb5ALT  44628  eexinst01  44629  ax6e2eq  44660  sineq0ALT  45039  tcfr  45066  ssclaxsep  45085  omssaxinf2  45091  nregmodel  45120  fzisoeu  45411  ovnsubaddlem2  46679  ormklocald  46982  natlocalincr  46984  tannpoly  47000  funressnfv  47153  faovcl  47310  sprsymrelfo  47607  clnbgrval  47932  gpgedgiov  48175  gpgedg2ov  48176  gpgedg2iv  48177  pgnioedg1  48218  pgnioedg2  48219  pgnioedg3  48220  pgnioedg4  48221  pgnioedg5  48222  pgnbgreunbgrlem2lem1  48224  pgnbgreunbgrlem2lem2  48225  pgnbgreunbgrlem2lem3  48226  pgnbgreunbgrlem5lem1  48230  pgnbgreunbgrlem5lem2  48231  cznnring  48372  zlmodzxznm  48608  elbigolo1  48668  dignn0flhalflem1  48726  nn0sumshdig  48734  rrx2xpref1o  48829  fonex  48977  vsetrec  49814