Theorem mpi 21

Description: A nested modus ponens inference. Inference associated with com12 33. (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 16	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  22  syl6mpi  68  mp2ani  710  mp3an3  1479  merco2  1766  equs4v  2030  alequexv  2031  equcomiv  2044  equcomi  2047  equvinva  2060  aeveq  2088  spimt  2418  equs4  2448  axc15  2454  2ax6elem  2502  dfeumo  2564  mo4  2594  sbcth  3759  sbcth2  3837  ssun3  4133  ssun4  4134  vn0  4298  elpreqprlem  4831  uniintsn  4950  sepexlem  5262  axprlem2  5395  axprlem4  5397  axpr  5398  axprlem1OLD  5399  axprlem3OLD  5400  axprlem4OLD  5401  axprlem5OLD  5402  axprOLD  5403  axprglem  5407  exel  5415  rext  5429  exss  5444  snopeqop  5489  propssopi  5491  uniopel  5499  opthhausdorff  5500  opthhausdorff0  5501  wefrc  5655  relopabi  5809  relop  5836  dmrnssfld  5964  iss  6037  sofld  6185  ordun  6467  funimass2  6619  fvbr0  6908  fvmptg  6987  funsndifnop  7148  ov3  7573  elovmpo  7655  dford5  7779  limsssuc  7842  tfisi  7851  finds1  7892  frxp  8118  frxp2  8136  frxp3  8143  dfrecs3  8355  tfrlem1  8358  oaordi  8527  oaword2  8534  omeulem1  8563  oeworde  8575  oelim2  8577  nnaordi  8600  oaabs2  8631  limenpsi  9136  dif1en  9142  ordunifi  9246  fidomdm  9287  dffi3  9387  oismo  9498  wdom2d  9538  wdomima2g  9544  epnsym  9574  suc11reg  9584  elom3  9613  cantnfval2  9634  rankunb  9818  rankval4  9835  karden  9877  cardsn  9951  cardlim  9954  cardprclem  9961  fseqdom  10006  dfac12lem3  10125  kmlem2  10131  kmlem10  10139  cflim2  10242  cfslb2n  10247  fin23lem27  10307  fin23lem17  10317  axcc3  10417  axcc4  10418  acncc  10419  domtriomlem  10421  axdclem2  10499  imadomg  10513  alephval2  10552  alephreg  10562  axextnd  10571  fpwwe2lem9  10619  pwfseq  10644  gch2  10655  axgroth3  10811  inaprc  10816  nlt1pi  10886  indpi  10887  1re  11203  mul02lem2  11382  addrid  11385  fimaxre  12154  fiminre  12157  supaddc  12177  supmul1  12179  rimul  12204  nnge1  12259  zneo  12674  ltweuz  13993  hashrabsn1  14406  hashf1lem2  14489  hash2pwpr  14509  climuni  15599  fsum2d  15818  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  fprod2d  16031  efne0d  16146  efne0OLD  16148  ruclem13  16293  dvdslelem  16362  mod2eq1n2dvds  16400  nn0o1gt2  16434  divalglem0  16446  lcmfnnval  16677  prmreclem2  16972  prmreclem3  16973  mreexexd  17699  coaval  18120  xpcco  18234  pltirr  18384  frgpnabllem1  19938  ablfac1eulem  20139  prmgrpsimpgd  20181  mdetunilem9  22777  mretopd  23249  fiuncmp  23561  ptcmpfi  23970  filtop  24012  supnfcls  24177  flimfnfcls  24185  alexsubALTlem2  24205  alexsubALTlem4  24207  trust  24386  rectbntr0  24990  fsumcn  25029  ovoliunlem3  25663  ovolicc2lem4  25679  dyadmax  25757  vitali  25772  itgfsum  25986  dvmptfsum  26134  fta1g  26327  fta1  26469  aannenlem1  26491  aalioulem3  26497  logltb  26765  logdmn0  26805  ang180lem2  26975  angpined  26995  mumullem2  27344  lgsqrmodndvds  27517  gausslemma2dlem0i  27528  2lgs  27571  dchrisum0re  27677  chpdifbnd  27719  pntrlog2bnd  27748  pntibndlem3  27756  pnt3  27776  nofv  27821  nomaxmo  27862  nominmo  27863  noprc  27949  madebday  28093  addsproplem7  28168  negsproplem7  28227  elons2  28451  nbgrval  29686  vtxdginducedm1fi  29894  upgrewlkle2  29956  hiidge0  31450  chsupval  31687  chsupcl  31692  chsupss  31694  ococin  31760  chsupval2  31762  ssjo  31799  h1de2i  31905  pjss2i  32032  pjssmii  32033  sto2i  32589  stge1i  32590  stle0i  32591  stlei  32592  stlesi  32593  stm1i  32595  staddi  32598  stadd3i  32600  golem1  32623  stcltrlem1  32628  mdexchi  32687  chirred  32747  atabsi  32753  abrexdomjm  32853  iocinif  33126  cycpmcl  33436  elrgspnsubrunlem2  33568  voliune  34619  volfiniune  34620  probdif  34810  bnj849  35313  axprALT2  35503  onvf1odlem4  35590  onvf1od  35591  onvfowev  35600  kur14lem9  35706  gonarlem  35886  gonar  35887  goalrlem  35888  goalr  35889  sscoid  36403  limsucncmpi  36976  axtco1from2  37006  axtcond  37009  bj-nnf-spime  37420  bj-axc10  37438  bj-alequex  37439  bj-spimtv  37449  bj-moeub  37504  bj-exlimvmpi  37566  bj-exlimmpi  37567  bj-restpw  37754  bj-isrvec  37958  finxpreclem4  38060  domalom  38070  wl-isseteq  38171  wl-embant  38185  wl-orel12  38186  wl-euequf  38249  poimirlem9  38300  abrexdom  38401  heiborlem10  38491  dvrunz  38625  iss2  39013  equcomi1  39694  ax12eq  39735  ax12el  39736  ax12inda  39742  ax12v2-o  39743  cvrnrefN  40076  pmod1i  40642  pmodN  40644  osumcllem11N  40760  pexmidlem8N  40771  pl42lem3N  40775  cdleme18b  41086  dochexmidlem8  42261  imadomfi  42789  sticksstones3  42935  sn-axprlem3  43009  sn-exelALT  43010  sn-1ne2  43052  remul02  43186  sn-0tie0  43245  pellexlem3  43578  pell1234qrne0  43600  hbtlem6  43876  onsucelab  44010  omabs2  44079  nadd2rabex  44133  or3or  44769  isotone1  44794  isotone2  44795  clsf2  44872  ismnushort  45031  radcnvrat  45044  3impexpbicom  45209  sb5ALT  45254  eexinst01  45255  ax6e2eq  45286  sineq0ALT  45665  tcfr  45692  ssclaxsep  45711  omssaxinf2  45717  nregmodel  45746  fzisoeu  46039  ovnsubaddlem2  47305  ormklocald  47610  natlocalincr  47612  tannpoly  47647  funressnfv  47800  faovcl  47957  sprsymrelfo  48266  clnbgrval  48607  gpgedgiov  48850  gpgedg2ov  48851  gpgedg2iv  48852  pgnioedg1  48893  pgnioedg2  48894  pgnioedg3  48895  pgnioedg4  48896  pgnioedg5  48897  pgnbgreunbgrlem2lem1  48899  pgnbgreunbgrlem2lem2  48900  pgnbgreunbgrlem2lem3  48901  pgnbgreunbgrlem5lem1  48905  pgnbgreunbgrlem5lem2  48906  cznnring  49047  zlmodzxznm  49297  elbigolo1  49357  dignn0flhalflem1  49415  nn0sumshdig  49423  rrx2xpref1o  49518  fonex  49665  vsetrec  50501