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  5235  axprlem2  5362  axprlem4  5364  axpr  5365  axprlem1OLD  5366  axprlem3OLD  5367  axprlem4OLD  5368  axprlem5OLD  5369  axprOLD  5370  axprglem  5374  exel  5382  rext  5396  exss  5411  snopeqop  5455  propssopi  5457  uniopel  5465  opthhausdorff  5466  opthhausdorff0  5467  wefrc  5619  relopabi  5772  relop  5800  dmrnssfld  5924  iss  5995  sofld  6146  ordun  6424  funimass2  6576  fvbr0  6862  fvmptg  6940  funsndifnop  7099  ov3  7524  elovmpo  7606  dford5  7732  limsssuc  7795  tfisi  7804  finds1  7844  frxp  8070  frxp2  8088  frxp3  8095  dfrecs3  8306  tfrlem1  8309  oaordi  8475  oaword2  8482  omeulem1  8511  oeworde  8523  oelim2  8525  nnaordi  8548  oaabs2  8579  limenpsi  9084  dif1en  9090  ordunifi  9194  fidomdm  9238  dffi3  9338  oismo  9449  wdom2d  9489  wdomima2g  9495  epnsym  9524  suc11reg  9534  elom3  9563  cantnfval2  9584  rankunb  9768  rankval4  9785  karden  9813  cardsn  9887  cardlim  9890  cardprclem  9897  fseqdom  9942  dfac12lem3  10062  kmlem2  10068  kmlem10  10076  cflim2  10179  cfslb2n  10184  fin23lem27  10244  fin23lem17  10254  axcc3  10354  axcc4  10355  acncc  10356  domtriomlem  10358  axdclem2  10436  imadomg  10450  alephval2  10489  alephreg  10499  axextnd  10508  fpwwe2lem9  10556  pwfseq  10581  gch2  10592  axgroth3  10748  inaprc  10753  nlt1pi  10823  indpi  10824  1re  11138  mul02lem2  11317  addrid  11320  fimaxre  12094  fiminre  12097  supaddc  12117  supmul1  12119  rimul  12144  nnge1  12199  zneo  12606  ltweuz  13917  hashrabsn1  14330  hashf1lem2  14412  hash2pwpr  14432  climuni  15508  fsum2d  15727  fsumabs  15758  fsumrlim  15768  fsumo1  15769  fsumiun  15778  fprod2d  15940  efne0d  16056  efne0OLD  16058  ruclem13  16203  dvdslelem  16272  mod2eq1n2dvds  16310  nn0o1gt2  16344  divalglem0  16356  lcmfnnval  16587  prmreclem2  16882  prmreclem3  16883  mreexexd  17608  coaval  18029  xpcco  18143  pltirr  18293  frgpnabllem1  19842  ablfac1eulem  20043  prmgrpsimpgd  20085  mdetunilem9  22598  mretopd  23070  fiuncmp  23382  ptcmpfi  23791  filtop  23833  supnfcls  23998  flimfnfcls  24006  alexsubALTlem2  24026  alexsubALTlem4  24028  trust  24207  rectbntr0  24811  fsumcn  24850  ovoliunlem3  25484  ovolicc2lem4  25500  dyadmax  25578  vitali  25593  itgfsum  25807  dvmptfsum  25955  fta1g  26148  fta1  26288  aannenlem1  26308  aalioulem3  26314  logltb  26580  logdmn0  26620  ang180lem2  26790  angpined  26810  mumullem2  27160  lgsqrmodndvds  27333  gausslemma2dlem0i  27344  2lgs  27387  dchrisum0re  27493  chpdifbnd  27535  pntrlog2bnd  27564  pntibndlem3  27572  pnt3  27592  nofv  27638  nomaxmo  27679  nominmo  27680  noprc  27765  madebday  27909  addsproplem7  27984  negsproplem7  28043  elons2  28267  nbgrval  29422  vtxdginducedm1fi  29631  upgrewlkle2  29693  hiidge0  31187  chsupval  31424  chsupcl  31429  chsupss  31431  ococin  31497  chsupval2  31499  ssjo  31536  h1de2i  31642  pjss2i  31769  pjssmii  31770  sto2i  32326  stge1i  32327  stle0i  32328  stlei  32329  stlesi  32330  stm1i  32332  staddi  32335  stadd3i  32337  golem1  32360  stcltrlem1  32365  mdexchi  32424  chirred  32484  atabsi  32490  abrexdomjm  32595  iocinif  32872  cycpmcl  33195  elrgspnsubrunlem2  33327  voliune  34392  volfiniune  34393  probdif  34583  bnj849  35086  axprALT2  35272  onvf1odlem4  35307  onvf1od  35308  kur14lem9  35415  gonarlem  35595  gonar  35596  goalrlem  35597  goalr  35598  sscoid  36112  limsucncmpi  36646  axtco1from2  36676  axtcond  36679  bj-nnf-spime  37091  bj-axc10  37109  bj-alequex  37110  bj-spimtv  37120  bj-moeub  37175  bj-exlimvmpi  37237  bj-exlimmpi  37238  bj-restpw  37423  bj-isrvec  37627  finxpreclem4  37727  domalom  37737  wl-isseteq  37838  wl-embant  37852  wl-orel12  37853  wl-euequf  37916  poimirlem9  37967  abrexdom  38068  heiborlem10  38158  dvrunz  38292  iss2  38682  equcomi1  39363  ax12eq  39404  ax12el  39405  ax12inda  39411  ax12v2-o  39412  cvrnrefN  39745  pmod1i  40311  pmodN  40313  osumcllem11N  40429  pexmidlem8N  40440  pl42lem3N  40444  cdleme18b  40755  dochexmidlem8  41930  imadomfi  42458  sticksstones3  42604  sn-axprlem3  42676  sn-exelALT  42677  sn-1ne2  42720  remul02  42854  sn-0tie0  42913  pellexlem3  43280  pell1234qrne0  43302  hbtlem6  43578  onsucelab  43712  omabs2  43781  nadd2rabex  43835  or3or  44471  isotone1  44496  isotone2  44497  clsf2  44574  ismnushort  44749  radcnvrat  44762  3impexpbicom  44928  sb5ALT  44973  eexinst01  44974  ax6e2eq  45005  sineq0ALT  45384  tcfr  45411  ssclaxsep  45430  omssaxinf2  45436  nregmodel  45465  fzisoeu  45754  ovnsubaddlem2  47020  ormklocald  47323  natlocalincr  47325  tannpoly  47353  funressnfv  47506  faovcl  47663  sprsymrelfo  47972  clnbgrval  48313  gpgedgiov  48556  gpgedg2ov  48557  gpgedg2iv  48558  pgnioedg1  48599  pgnioedg2  48600  pgnioedg3  48601  pgnioedg4  48602  pgnioedg5  48603  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  pgnbgreunbgrlem5lem1  48611  pgnbgreunbgrlem5lem2  48612  cznnring  48753  zlmodzxznm  48988  elbigolo1  49048  dignn0flhalflem1  49106  nn0sumshdig  49114  rrx2xpref1o  49209  fonex  49357  vsetrec  50193