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  697  mp3an3  1450  merco2  1734  equs4v  1999  alequexv  2000  equcomiv  2013  equcomi  2016  equvinva  2029  aeveq  2056  spimt  2394  equs4  2424  axc15  2430  2ax6elem  2478  dfeumo  2540  mo4  2569  sbcth  3819  sbcth2  3906  ssun3  4203  ssun4  4204  elpreqprlem  4890  uniintsn  5009  axprlem1  5441  axprlem2  5442  axprlem3  5443  axprlem4  5444  axprlem5  5445  axpr  5446  exel  5453  rext  5468  exss  5483  snopeqop  5525  propssopi  5527  uniopel  5535  opthhausdorff  5536  opthhausdorff0  5537  wefrc  5694  relopabi  5846  relop  5875  dmrnssfld  5996  iss  6064  sofld  6218  ordun  6499  funimass2  6661  fvbr0  6949  fvmptg  7027  funsndifnop  7185  ov3  7613  elovmpo  7695  dford5  7819  limsssuc  7887  tfisi  7896  finds1  7939  frxp  8167  frxp2  8185  frxp3  8192  wfrlem5OLD  8369  wfrlem16OLD  8380  dfrecs3  8428  dfrecs3OLD  8429  tfrlem1  8432  oaordi  8602  oaword2  8609  omeulem1  8638  oeworde  8649  oelim2  8651  nnaordi  8674  oaabs2  8705  0domgOLD  9167  limenpsi  9218  dif1en  9226  dif1enOLD  9228  enp1iOLD  9342  ordunifi  9354  fidomdm  9402  dffi3  9500  oismo  9609  wdom2d  9649  wdomima2g  9655  epnsym  9678  suc11reg  9688  elom3  9717  cantnfval2  9738  rankunb  9919  rankval4  9936  karden  9964  cardsn  10038  cardlim  10041  cardprclem  10048  fseqdom  10095  dfac12lem3  10215  kmlem2  10221  kmlem10  10229  cflim2  10332  cfslb2n  10337  fin23lem27  10397  fin23lem17  10407  axcc3  10507  axcc4  10508  acncc  10509  domtriomlem  10511  axdclem2  10589  imadomg  10603  alephval2  10641  alephreg  10651  axextnd  10660  fpwwe2lem9  10708  pwfseq  10733  gch2  10744  axgroth3  10900  inaprc  10905  nlt1pi  10975  indpi  10976  1re  11290  mul02lem2  11467  addrid  11470  fimaxre  12239  fiminre  12242  supaddc  12262  supmul1  12264  inelr  12283  rimul  12284  nnge1  12321  zneo  12726  ltweuz  14012  hashrabsn1  14423  hashf1lem2  14505  hash2pwpr  14525  climuni  15598  fsum2d  15819  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  fprod2d  16029  efne0  16145  ruclem13  16290  dvdslelem  16357  mod2eq1n2dvds  16395  nn0o1gt2  16429  divalglem0  16441  lcmfnnval  16671  prmreclem2  16964  prmreclem3  16965  mreexexd  17706  coaval  18135  xpcco  18252  pltirr  18405  frgpnabllem1  19915  ablfac1eulem  20116  prmgrpsimpgd  20158  mdetunilem9  22647  mretopd  23121  fiuncmp  23433  ptcmpfi  23842  filtop  23884  supnfcls  24049  flimfnfcls  24057  alexsubALTlem2  24077  alexsubALTlem4  24079  trust  24259  rectbntr0  24873  fsumcn  24913  ovoliunlem3  25558  ovolicc2lem4  25574  dyadmax  25652  vitali  25667  itgfsum  25882  dvmptfsum  26033  fta1g  26229  fta1  26368  aannenlem1  26388  aalioulem3  26394  logltb  26660  logdmn0  26700  ang180lem2  26871  angpined  26891  mumullem2  27241  lgsqrmodndvds  27415  gausslemma2dlem0i  27426  2lgs  27469  dchrisum0re  27575  chpdifbnd  27617  pntrlog2bnd  27646  pntibndlem3  27654  pnt3  27674  nofv  27720  nomaxmo  27761  nominmo  27762  noprc  27842  madebday  27956  addsproplem7  28026  negsproplem7  28084  elons2  28299  nbgrval  29371  vtxdginducedm1fi  29580  upgrewlkle2  29642  hiidge0  31130  chsupval  31367  chsupcl  31372  chsupss  31374  ococin  31440  chsupval2  31442  ssjo  31479  h1de2i  31585  pjss2i  31712  pjssmii  31713  sto2i  32269  stge1i  32270  stle0i  32271  stlei  32272  stlesi  32273  stm1i  32275  staddi  32278  stadd3i  32280  golem1  32303  stcltrlem1  32308  mdexchi  32367  chirred  32427  atabsi  32433  abrexdomjm  32535  iocinif  32786  cycpmcl  33109  voliune  34193  volfiniune  34194  probdif  34385  bnj849  34901  kur14lem9  35182  gonarlem  35362  gonar  35363  goalrlem  35364  goalr  35365  sscoid  35877  limsucncmpi  36411  bj-axc10  36749  bj-alequex  36750  bj-spimtv  36760  bj-moeub  36815  bj-exlimvmpi  36877  bj-exlimmpi  36878  bj-restpw  37058  bj-isrvec  37260  finxpreclem4  37360  domalom  37370  wl-embant  37464  wl-orel12  37465  wl-euequf  37528  poimirlem9  37589  abrexdom  37690  heiborlem10  37780  dvrunz  37914  iss2  38300  equcomi1  38856  ax12eq  38897  ax12el  38898  ax12inda  38904  ax12v2-o  38905  cvrnrefN  39238  pmod1i  39805  pmodN  39807  osumcllem11N  39923  pexmidlem8N  39934  pl42lem3N  39938  cdleme18b  40249  dochexmidlem8  41424  imadomfi  41959  sticksstones3  42105  sn-axprlem3  42210  sn-exelALT  42211  sn-1ne2  42254  efne0d  42325  remul02  42381  sn-0tie0  42415  pellexlem3  42787  pell1234qrne0  42809  hbtlem6  43086  onsucelab  43225  omabs2  43294  nadd2rabex  43348  or3or  43985  isotone1  44010  isotone2  44011  clsf2  44088  ismnushort  44270  radcnvrat  44283  3impexpbicom  44450  sb5ALT  44496  eexinst01  44497  ax6e2eq  44528  sineq0ALT  44908  fzisoeu  45215  ovnsubaddlem2  46492  natlocalincr  46795  tworepnotupword  46805  funressnfv  46958  faovcl  47115  sprsymrelfo  47371  clnbgrval  47696  cznnring  47985  zlmodzxznm  48226  elbigolo1  48291  dignn0flhalflem1  48349  nn0sumshdig  48357  rrx2xpref1o  48452  vsetrec  48795