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  696  mp3an3  1446  merco2  1733  equs4v  2002  alequexv  2003  equcomiv  2017  equcomi  2020  equvinva  2033  aeveq  2057  spsbeOLD  2085  spimt  2400  equs4  2434  axc15  2440  2ax6elem  2489  dfeumo  2615  mo4  2646  pm13.183  3658  pm13.183OLD  3659  sbcth  3786  sbcth2  3866  ssun3  4149  ssun4  4150  elpreqprlem  4795  uniintsn  4912  axprlem1  5323  axprlem2  5324  axprlem3  5325  axprlem4  5326  axprlem5  5327  axpr  5328  rext  5340  exss  5354  snopeqop  5395  propssopi  5397  uniopel  5405  opthhausdorff  5406  opthhausdorff0  5407  wefrc  5548  relopabi  5693  relop  5720  dmrnssfld  5840  iss  5902  sofld  6043  ordun  6291  funimass2  6436  fvbr0  6696  fvmptg  6765  funsndifnop  6912  fovcl  7278  ov3  7310  elovmpo  7389  limsssuc  7564  tfisi  7572  finds1  7610  frxp  7819  wfrlem5  7958  wfrlem16  7969  dfrecs3  8008  tfrlem1  8011  oaordi  8171  oaword2  8178  omeulem1  8207  oeworde  8218  oelim2  8220  nnaordi  8243  oaabs2  8271  0domg  8643  limenpsi  8691  enp1i  8752  findcard2  8757  ordunifi  8767  fidomdm  8800  dffi3  8894  oismo  9003  wdom2d  9043  wdomima2g  9049  epnsym  9071  suc11reg  9081  elom3  9110  cantnfval2  9131  rankunb  9278  rankval4  9295  karden  9323  cardsn  9397  cardlim  9400  cardprclem  9407  fseqdom  9451  dfac12lem3  9570  kmlem2  9576  kmlem10  9584  cflim2  9684  cfslb2n  9689  fin23lem27  9749  fin23lem17  9759  axcc3  9859  axcc4  9860  acncc  9861  domtriomlem  9863  axdclem2  9941  imadomg  9955  alephval2  9993  alephreg  10003  axextnd  10012  fpwwe2lem10  10060  pwfseq  10085  gch2  10096  axgroth3  10252  inaprc  10257  nlt1pi  10327  indpi  10328  1re  10640  mul02lem2  10816  addid1  10819  fimaxre  11583  fimaxreOLD  11584  fiminre  11587  supaddc  11607  supmul1  11609  inelr  11627  rimul  11628  nnge1  11664  nnne0  11670  zneo  12064  ltweuz  13328  hashrabsn1  13734  hashf1lem2  13813  hash2pwpr  13833  climuni  14908  fsum2d  15125  fsumabs  15155  fsumrlim  15165  fsumo1  15166  fsumiun  15175  fprod2d  15334  efne0  15449  ruclem13  15594  dvdslelem  15658  mod2eq1n2dvds  15695  nn0o1gt2  15731  divalglem0  15743  lcmfnnval  15967  prmreclem2  16252  prmreclem3  16253  mreexexd  16918  coaval  17327  xpcco  17432  pltirr  17572  frgpnabllem1  18992  ablfac1eulem  19193  prmgrpsimpgd  19235  mdetunilem9  21228  mretopd  21699  fiuncmp  22011  ptcmpfi  22420  filtop  22462  supnfcls  22627  flimfnfcls  22635  alexsubALTlem2  22655  alexsubALTlem4  22657  trust  22837  rectbntr0  23439  fsumcn  23477  ovoliunlem3  24104  ovolicc2lem4  24120  dyadmax  24198  vitali  24213  itgfsum  24426  dvmptfsum  24571  fta1g  24760  fta1  24896  aannenlem1  24916  aalioulem3  24922  logltb  25182  logdmn0  25222  ang180lem2  25387  angpined  25407  mumullem2  25756  lgsqrmodndvds  25928  gausslemma2dlem0i  25939  2lgs  25982  dchrisum0re  26088  chpdifbnd  26130  pntrlog2bnd  26159  pntibndlem3  26167  pnt3  26187  nbgrval  27117  vtxdginducedm1fi  27325  upgrewlkle2  27387  hiidge0  28874  chsupval  29111  chsupcl  29116  chsupss  29118  ococin  29184  chsupval2  29186  ssjo  29223  h1de2i  29329  pjss2i  29456  pjssmii  29457  sto2i  30013  stge1i  30014  stle0i  30015  stlei  30016  stlesi  30017  stm1i  30019  staddi  30022  stadd3i  30024  golem1  30047  stcltrlem1  30052  mdexchi  30111  chirred  30171  atabsi  30177  abrexdomjm  30266  iocinif  30503  cycpmcl  30758  voliune  31488  volfiniune  31489  probdif  31678  bnj849  32197  kur14lem9  32461  gonarlem  32641  gonar  32642  goalrlem  32643  goalr  32644  dford5  32957  nofv  33164  nomaxmo  33201  noprc  33249  sscoid  33374  limsucncmpi  33793  bj-axc10  34105  bj-alequex  34106  bj-spimtv  34116  bj-moeub  34173  bj-exlimvmpi  34227  bj-exlimmpi  34228  bj-restpw  34382  finxpreclem4  34674  domalom  34684  wl-embant  34749  wl-orel12  34750  wl-euequf  34809  poimirlem9  34900  abrexdom  35004  heiborlem10  35097  dvrunz  35231  iss2  35600  equcomi1  36035  ax12eq  36076  ax12el  36077  ax12inda  36083  ax12v2-o  36084  cvrnrefN  36417  pmod1i  36983  pmodN  36985  osumcllem11N  37101  pexmidlem8N  37112  pl42lem3N  37116  cdleme18b  37427  dochexmidlem8  38602  sn-axprlem3  39107  sn-el  39108  sn-1ne2  39156  remul02  39233  pellexlem3  39426  pell1234qrne0  39448  hbtlem6  39727  or3or  40369  isotone1  40396  isotone2  40397  clsf2  40474  radcnvrat  40644  3impexpbicom  40811  sb5ALT  40857  eexinst01  40858  ax6e2eq  40889  sineq0ALT  41269  fzisoeu  41565  ovnsubaddlem2  42852  funressnfv  43277  faovcl  43398  sprsymrelfo  43658  cznnring  44226  zlmodzxznm  44551  elbigolo1  44616  dignn0flhalflem1  44674  nn0sumshdig  44682  rrx2xpref1o  44704  vsetrec  44804