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  1447  merco2  1738  equs4v  2006  alequexv  2007  equcomiv  2021  equcomi  2024  equvinva  2037  aeveq  2061  spimt  2393  equs4  2427  axc15  2433  2ax6elem  2482  dfeumo  2595  mo4  2625  pm13.183  3606  sbcth  3735  sbcth2  3813  ssun3  4101  ssun4  4102  elpreqprlem  4756  uniintsn  4875  axprlem1  5289  axprlem2  5290  axprlem3  5291  axprlem4  5292  axprlem5  5293  axpr  5294  rext  5306  exss  5320  snopeqop  5361  propssopi  5363  uniopel  5371  opthhausdorff  5372  opthhausdorff0  5373  wefrc  5513  relopabi  5658  relop  5685  dmrnssfld  5806  iss  5870  sofld  6011  ordun  6260  funimass2  6407  fvbr0  6672  fvmptg  6743  funsndifnop  6890  fovcl  7258  ov3  7291  elovmpo  7370  limsssuc  7545  tfisi  7553  finds1  7592  frxp  7803  wfrlem5  7942  wfrlem16  7953  dfrecs3  7992  tfrlem1  7995  oaordi  8155  oaword2  8162  omeulem1  8191  oeworde  8202  oelim2  8204  nnaordi  8227  oaabs2  8255  0domg  8628  limenpsi  8676  enp1i  8737  findcard2  8742  ordunifi  8752  fidomdm  8785  dffi3  8879  oismo  8988  wdom2d  9028  wdomima2g  9034  epnsym  9056  suc11reg  9066  elom3  9095  cantnfval2  9116  rankunb  9263  rankval4  9280  karden  9308  cardsn  9382  cardlim  9385  cardprclem  9392  fseqdom  9437  dfac12lem3  9556  kmlem2  9562  kmlem10  9570  cflim2  9674  cfslb2n  9679  fin23lem27  9739  fin23lem17  9749  axcc3  9849  axcc4  9850  acncc  9851  domtriomlem  9853  axdclem2  9931  imadomg  9945  alephval2  9983  alephreg  9993  axextnd  10002  fpwwe2lem10  10050  pwfseq  10075  gch2  10086  axgroth3  10242  inaprc  10247  nlt1pi  10317  indpi  10318  1re  10630  mul02lem2  10806  addid1  10809  fimaxre  11573  fiminre  11576  supaddc  11595  supmul1  11597  inelr  11615  rimul  11616  nnge1  11653  nnne0  11659  zneo  12053  ltweuz  13324  hashrabsn1  13731  hashf1lem2  13810  hash2pwpr  13830  climuni  14901  fsum2d  15118  fsumabs  15148  fsumrlim  15158  fsumo1  15159  fsumiun  15168  fprod2d  15327  efne0  15442  ruclem13  15587  dvdslelem  15651  mod2eq1n2dvds  15688  nn0o1gt2  15722  divalglem0  15734  lcmfnnval  15958  prmreclem2  16243  prmreclem3  16244  mreexexd  16911  coaval  17320  xpcco  17425  pltirr  17565  frgpnabllem1  18986  ablfac1eulem  19187  prmgrpsimpgd  19229  mdetunilem9  21225  mretopd  21697  fiuncmp  22009  ptcmpfi  22418  filtop  22460  supnfcls  22625  flimfnfcls  22633  alexsubALTlem2  22653  alexsubALTlem4  22655  trust  22835  rectbntr0  23437  fsumcn  23475  ovoliunlem3  24108  ovolicc2lem4  24124  dyadmax  24202  vitali  24217  itgfsum  24430  dvmptfsum  24578  fta1g  24768  fta1  24904  aannenlem1  24924  aalioulem3  24930  logltb  25191  logdmn0  25231  ang180lem2  25396  angpined  25416  mumullem2  25765  lgsqrmodndvds  25937  gausslemma2dlem0i  25948  2lgs  25991  dchrisum0re  26097  chpdifbnd  26139  pntrlog2bnd  26168  pntibndlem3  26176  pnt3  26196  nbgrval  27126  vtxdginducedm1fi  27334  upgrewlkle2  27396  hiidge0  28881  chsupval  29118  chsupcl  29123  chsupss  29125  ococin  29191  chsupval2  29193  ssjo  29230  h1de2i  29336  pjss2i  29463  pjssmii  29464  sto2i  30020  stge1i  30021  stle0i  30022  stlei  30023  stlesi  30024  stm1i  30026  staddi  30029  stadd3i  30031  golem1  30054  stcltrlem1  30059  mdexchi  30118  chirred  30178  atabsi  30184  abrexdomjm  30275  iocinif  30530  cycpmcl  30808  voliune  31598  volfiniune  31599  probdif  31788  bnj849  32307  kur14lem9  32574  gonarlem  32754  gonar  32755  goalrlem  32756  goalr  32757  dford5  33070  nofv  33277  nomaxmo  33314  noprc  33362  sscoid  33487  limsucncmpi  33906  bj-axc10  34220  bj-alequex  34221  bj-spimtv  34231  bj-moeub  34288  bj-exlimvmpi  34351  bj-exlimmpi  34352  bj-restpw  34507  finxpreclem4  34811  domalom  34821  wl-embant  34915  wl-orel12  34916  wl-euequf  34975  poimirlem9  35066  abrexdom  35168  heiborlem10  35258  dvrunz  35392  iss2  35761  equcomi1  36196  ax12eq  36237  ax12el  36238  ax12inda  36244  ax12v2-o  36245  cvrnrefN  36578  pmod1i  37144  pmodN  37146  osumcllem11N  37262  pexmidlem8N  37273  pl42lem3N  37277  cdleme18b  37588  dochexmidlem8  38763  sn-axprlem3  39401  sn-el  39402  sn-1ne2  39466  remul02  39543  sn-0tie0  39576  pellexlem3  39772  pell1234qrne0  39794  hbtlem6  40073  or3or  40724  isotone1  40751  isotone2  40752  clsf2  40829  radcnvrat  41018  3impexpbicom  41185  sb5ALT  41231  eexinst01  41232  ax6e2eq  41263  sineq0ALT  41643  fzisoeu  41932  ovnsubaddlem2  43210  funressnfv  43635  faovcl  43756  sprsymrelfo  44014  cznnring  44580  zlmodzxznm  44906  elbigolo1  44971  dignn0flhalflem1  45029  nn0sumshdig  45037  rrx2xpref1o  45132  vsetrec  45232