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  694  mp3an3  1448  merco2  1740  equs4v  2004  alequexv  2005  equcomiv  2018  equcomi  2021  equvinva  2034  aeveq  2060  spimt  2386  equs4  2416  axc15  2422  2ax6elem  2470  dfeumo  2537  mo4  2566  pm13.183  3590  sbcth  3726  sbcth2  3813  ssun3  4104  ssun4  4105  elpreqprlem  4793  uniintsn  4915  axprlem1  5341  axprlem2  5342  axprlem3  5343  axprlem4  5344  axprlem5  5345  axpr  5346  rext  5358  exss  5372  snopeqop  5414  propssopi  5416  uniopel  5424  opthhausdorff  5425  opthhausdorff0  5426  wefrc  5574  relopabi  5721  relop  5748  dmrnssfld  5868  iss  5932  sofld  6079  ordun  6352  funimass2  6501  fvbr0  6783  fvmptg  6855  funsndifnop  7005  fovcl  7380  ov3  7413  elovmpo  7492  limsssuc  7672  tfisi  7680  finds1  7722  frxp  7938  wfrlem5OLD  8115  wfrlem16OLD  8126  dfrecs3  8174  dfrecs3OLD  8175  tfrlem1  8178  oaordi  8339  oaword2  8346  omeulem1  8375  oeworde  8386  oelim2  8388  nnaordi  8411  oaabs2  8439  0domg  8840  limenpsi  8888  dif1en  8907  enp1i  8982  findcard2OLD  8986  ordunifi  8994  fidomdm  9026  dffi3  9120  oismo  9229  wdom2d  9269  wdomima2g  9275  epnsym  9297  suc11reg  9307  elom3  9336  cantnfval2  9357  rankunb  9539  rankval4  9556  karden  9584  cardsn  9658  cardlim  9661  cardprclem  9668  fseqdom  9713  dfac12lem3  9832  kmlem2  9838  kmlem10  9846  cflim2  9950  cfslb2n  9955  fin23lem27  10015  fin23lem17  10025  axcc3  10125  axcc4  10126  acncc  10127  domtriomlem  10129  axdclem2  10207  imadomg  10221  alephval2  10259  alephreg  10269  axextnd  10278  fpwwe2lem9  10326  pwfseq  10351  gch2  10362  axgroth3  10518  inaprc  10523  nlt1pi  10593  indpi  10594  1re  10906  mul02lem2  11082  addid1  11085  fimaxre  11849  fiminre  11852  supaddc  11872  supmul1  11874  inelr  11893  rimul  11894  nnge1  11931  nnne0  11937  zneo  12333  ltweuz  13609  hashrabsn1  14017  hashf1lem2  14098  hash2pwpr  14118  climuni  15189  fsum2d  15411  fsumabs  15441  fsumrlim  15451  fsumo1  15452  fsumiun  15461  fprod2d  15619  efne0  15734  ruclem13  15879  dvdslelem  15946  mod2eq1n2dvds  15984  nn0o1gt2  16018  divalglem0  16030  lcmfnnval  16257  prmreclem2  16546  prmreclem3  16547  mreexexd  17274  coaval  17699  xpcco  17816  pltirr  17968  frgpnabllem1  19389  ablfac1eulem  19590  prmgrpsimpgd  19632  mdetunilem9  21677  mretopd  22151  fiuncmp  22463  ptcmpfi  22872  filtop  22914  supnfcls  23079  flimfnfcls  23087  alexsubALTlem2  23107  alexsubALTlem4  23109  trust  23289  rectbntr0  23901  fsumcn  23939  ovoliunlem3  24573  ovolicc2lem4  24589  dyadmax  24667  vitali  24682  itgfsum  24896  dvmptfsum  25044  fta1g  25237  fta1  25373  aannenlem1  25393  aalioulem3  25399  logltb  25660  logdmn0  25700  ang180lem2  25865  angpined  25885  mumullem2  26234  lgsqrmodndvds  26406  gausslemma2dlem0i  26417  2lgs  26460  dchrisum0re  26566  chpdifbnd  26608  pntrlog2bnd  26637  pntibndlem3  26645  pnt3  26665  nbgrval  27606  vtxdginducedm1fi  27814  upgrewlkle2  27876  hiidge0  29361  chsupval  29598  chsupcl  29603  chsupss  29605  ococin  29671  chsupval2  29673  ssjo  29710  h1de2i  29816  pjss2i  29943  pjssmii  29944  sto2i  30500  stge1i  30501  stle0i  30502  stlei  30503  stlesi  30504  stm1i  30506  staddi  30509  stadd3i  30511  golem1  30534  stcltrlem1  30539  mdexchi  30598  chirred  30658  atabsi  30664  abrexdomjm  30753  iocinif  31004  cycpmcl  31285  voliune  32097  volfiniune  32098  probdif  32287  bnj849  32805  kur14lem9  33076  gonarlem  33256  gonar  33257  goalrlem  33258  goalr  33259  dford5  33573  frxp2  33718  nofv  33787  nomaxmo  33828  nominmo  33829  noprc  33901  madebday  34007  sscoid  34142  limsucncmpi  34561  bj-axc10  34892  bj-alequex  34893  bj-spimtv  34903  bj-moeub  34960  bj-exlimvmpi  35023  bj-exlimmpi  35024  bj-restpw  35190  bj-isrvec  35392  finxpreclem4  35492  domalom  35502  wl-embant  35596  wl-orel12  35597  wl-euequf  35656  poimirlem9  35713  abrexdom  35815  heiborlem10  35905  dvrunz  36039  iss2  36406  equcomi1  36841  ax12eq  36882  ax12el  36883  ax12inda  36889  ax12v2-o  36890  cvrnrefN  37223  pmod1i  37789  pmodN  37791  osumcllem11N  37907  pexmidlem8N  37918  pl42lem3N  37922  cdleme18b  38233  dochexmidlem8  39408  sticksstones3  40032  sn-axprlem3  40114  sn-el  40115  sn-1ne2  40216  remul02  40309  sn-0tie0  40342  pellexlem3  40569  pell1234qrne0  40591  hbtlem6  40870  or3or  41520  isotone1  41547  isotone2  41548  clsf2  41625  ismnushort  41808  radcnvrat  41821  3impexpbicom  41988  sb5ALT  42034  eexinst01  42035  ax6e2eq  42066  sineq0ALT  42446  fzisoeu  42729  ovnsubaddlem2  43999  funressnfv  44424  faovcl  44579  sprsymrelfo  44837  cznnring  45402  zlmodzxznm  45726  elbigolo1  45791  dignn0flhalflem1  45849  nn0sumshdig  45857  rrx2xpref1o  45952  vsetrec  46294