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  1476  merco2  1763  equs4v  2027  alequexv  2028  equcomiv  2041  equcomi  2044  equvinva  2057  aeveq  2085  spimt  2424  equs4  2454  axc15  2460  2ax6elem  2508  dfeumo  2570  mo4  2600  sbcth  3768  sbcth2  3846  ssun3  4141  ssun4  4142  vn0  4306  elpreqprlem  4835  uniintsn  4954  sepexlem  5264  axprlem2  5396  axprlem4  5398  axpr  5399  axprlem1OLD  5400  axprlem3OLD  5401  axprlem4OLD  5402  axprlem5OLD  5403  axprOLD  5404  axprglem  5408  exel  5416  rext  5430  exss  5445  snopeqop  5490  propssopi  5492  uniopel  5500  opthhausdorff  5501  opthhausdorff0  5502  wefrc  5656  relopabi  5810  relop  5837  dmrnssfld  5965  iss  6038  sofld  6186  ordun  6468  funimass2  6620  fvbr0  6909  fvmptg  6988  funsndifnop  7149  ov3  7574  elovmpo  7656  dford5  7783  limsssuc  7846  tfisi  7855  finds1  7896  frxp  8122  frxp2  8140  frxp3  8147  dfrecs3  8359  tfrlem1  8362  oaordi  8531  oaword2  8538  omeulem1  8567  oeworde  8579  oelim2  8581  nnaordi  8604  oaabs2  8635  limenpsi  9140  dif1en  9146  ordunifi  9250  fidomdm  9291  dffi3  9391  oismo  9502  wdom2d  9542  wdomima2g  9548  epnsym  9578  suc11reg  9588  elom3  9617  cantnfval2  9638  rankunb  9822  rankval4  9839  karden  9881  cardsn  9955  cardlim  9958  cardprclem  9965  fseqdom  10010  dfac12lem3  10129  kmlem2  10135  kmlem10  10143  cflim2  10247  cfslb2n  10252  fin23lem27  10312  fin23lem17  10322  axcc3  10422  axcc4  10423  acncc  10424  domtriomlem  10426  axdclem2  10504  imadomg  10518  alephval2  10557  alephreg  10567  axextnd  10576  fpwwe2lem9  10624  pwfseq  10649  gch2  10660  axgroth3  10816  inaprc  10821  nlt1pi  10891  indpi  10892  1re  11208  mul02lem2  11387  addrid  11390  fimaxre  12159  fiminre  12162  supaddc  12182  supmul1  12184  rimul  12209  nnge1  12264  zneo  12679  ltweuz  13997  hashrabsn1  14410  hashf1lem2  14493  hash2pwpr  14513  climuni  15603  fsum2d  15822  fsumabs  15853  fsumrlim  15863  fsumo1  15864  fsumiun  15873  fprod2d  16035  efne0d  16151  efne0OLD  16153  ruclem13  16298  dvdslelem  16367  mod2eq1n2dvds  16405  nn0o1gt2  16439  divalglem0  16451  lcmfnnval  16682  prmreclem2  16977  prmreclem3  16978  mreexexd  17704  coaval  18125  xpcco  18239  pltirr  18389  frgpnabllem1  19943  ablfac1eulem  20144  prmgrpsimpgd  20186  mdetunilem9  22746  mretopd  23218  fiuncmp  23530  ptcmpfi  23939  filtop  23981  supnfcls  24146  flimfnfcls  24154  alexsubALTlem2  24174  alexsubALTlem4  24176  trust  24355  rectbntr0  24959  fsumcn  24998  ovoliunlem3  25632  ovolicc2lem4  25648  dyadmax  25726  vitali  25741  itgfsum  25955  dvmptfsum  26103  fta1g  26296  fta1  26438  aannenlem1  26458  aalioulem3  26464  logltb  26731  logdmn0  26771  ang180lem2  26941  angpined  26961  mumullem2  27310  lgsqrmodndvds  27483  gausslemma2dlem0i  27494  2lgs  27537  dchrisum0re  27643  chpdifbnd  27685  pntrlog2bnd  27714  pntibndlem3  27722  pnt3  27742  nofv  27787  nomaxmo  27828  nominmo  27829  noprc  27915  madebday  28059  addsproplem7  28134  negsproplem7  28193  elons2  28417  nbgrval  29627  vtxdginducedm1fi  29835  upgrewlkle2  29897  hiidge0  31391  chsupval  31628  chsupcl  31633  chsupss  31635  ococin  31701  chsupval2  31703  ssjo  31740  h1de2i  31846  pjss2i  31973  pjssmii  31974  sto2i  32530  stge1i  32531  stle0i  32532  stlei  32533  stlesi  32534  stm1i  32536  staddi  32539  stadd3i  32541  golem1  32564  stcltrlem1  32569  mdexchi  32628  chirred  32688  atabsi  32694  abrexdomjm  32794  iocinif  33067  cycpmcl  33377  elrgspnsubrunlem2  33509  voliune  34564  volfiniune  34565  probdif  34755  bnj849  35258  axprALT2  35446  onvf1odlem4  35523  onvf1od  35524  onvfowev  35533  kur14lem9  35639  gonarlem  35819  gonar  35820  goalrlem  35821  goalr  35822  sscoid  36336  limsucncmpi  36879  axtco1from2  36909  axtcond  36912  bj-nnf-spime  37323  bj-axc10  37341  bj-alequex  37342  bj-spimtv  37352  bj-moeub  37407  bj-exlimvmpi  37469  bj-exlimmpi  37470  bj-restpw  37656  bj-isrvec  37860  finxpreclem4  37962  domalom  37972  wl-isseteq  38073  wl-embant  38087  wl-orel12  38088  wl-euequf  38151  poimirlem9  38202  abrexdom  38303  heiborlem10  38393  dvrunz  38527  iss2  38917  equcomi1  39598  ax12eq  39639  ax12el  39640  ax12inda  39646  ax12v2-o  39647  cvrnrefN  39980  pmod1i  40546  pmodN  40548  osumcllem11N  40664  pexmidlem8N  40675  pl42lem3N  40679  cdleme18b  40990  dochexmidlem8  42165  imadomfi  42693  sticksstones3  42839  sn-axprlem3  42913  sn-exelALT  42914  sn-1ne2  42956  remul02  43090  sn-0tie0  43149  pellexlem3  43484  pell1234qrne0  43506  hbtlem6  43782  onsucelab  43916  omabs2  43985  nadd2rabex  44039  or3or  44675  isotone1  44700  isotone2  44701  clsf2  44778  ismnushort  44937  radcnvrat  44950  3impexpbicom  45115  sb5ALT  45160  eexinst01  45161  ax6e2eq  45192  sineq0ALT  45571  tcfr  45598  ssclaxsep  45617  omssaxinf2  45623  nregmodel  45652  fzisoeu  45945  ovnsubaddlem2  47211  ormklocald  47516  natlocalincr  47518  tannpoly  47550  funressnfv  47703  faovcl  47860  sprsymrelfo  48169  clnbgrval  48510  gpgedgiov  48753  gpgedg2ov  48754  gpgedg2iv  48755  pgnioedg1  48796  pgnioedg2  48797  pgnioedg3  48798  pgnioedg4  48799  pgnioedg5  48800  pgnbgreunbgrlem2lem1  48802  pgnbgreunbgrlem2lem2  48803  pgnbgreunbgrlem2lem3  48804  pgnbgreunbgrlem5lem1  48808  pgnbgreunbgrlem5lem2  48809  cznnring  48950  zlmodzxznm  49196  elbigolo1  49256  dignn0flhalflem1  49314  nn0sumshdig  49322  rrx2xpref1o  49417  fonex  49564  vsetrec  50400