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  698  mp3an3  1451  merco2  1735  equs4v  1998  alequexv  1999  equcomiv  2012  equcomi  2015  equvinva  2028  aeveq  2055  spimt  2389  equs4  2419  axc15  2425  2ax6elem  2473  dfeumo  2535  mo4  2564  sbcth  3785  sbcth2  3864  ssun3  4160  ssun4  4161  elpreqprlem  4846  uniintsn  4965  sepexlem  5279  axprlem1  5403  axprlem2  5404  axprlem4  5406  axpr  5407  axprlem3OLD  5408  axprlem4OLD  5409  axprlem5OLD  5410  axprOLD  5411  exel  5418  rext  5433  exss  5448  snopeqop  5491  propssopi  5493  uniopel  5501  opthhausdorff  5502  opthhausdorff0  5503  wefrc  5659  relopabi  5812  relop  5841  dmrnssfld  5964  iss  6033  sofld  6187  ordun  6468  funimass2  6629  fvbr0  6915  fvmptg  6994  funsndifnop  7151  ov3  7578  elovmpo  7660  dford5  7786  limsssuc  7853  tfisi  7862  finds1  7903  frxp  8133  frxp2  8151  frxp3  8158  wfrlem5OLD  8335  wfrlem16OLD  8346  dfrecs3  8394  dfrecs3OLD  8395  tfrlem1  8398  oaordi  8566  oaword2  8573  omeulem1  8602  oeworde  8613  oelim2  8615  nnaordi  8638  oaabs2  8669  0domgOLD  9123  limenpsi  9174  dif1en  9182  dif1enOLD  9184  enp1iOLD  9296  ordunifi  9308  fidomdm  9356  dffi3  9453  oismo  9562  wdom2d  9602  wdomima2g  9608  epnsym  9631  suc11reg  9641  elom3  9670  cantnfval2  9691  rankunb  9872  rankval4  9889  karden  9917  cardsn  9991  cardlim  9994  cardprclem  10001  fseqdom  10048  dfac12lem3  10168  kmlem2  10174  kmlem10  10182  cflim2  10285  cfslb2n  10290  fin23lem27  10350  fin23lem17  10360  axcc3  10460  axcc4  10461  acncc  10462  domtriomlem  10464  axdclem2  10542  imadomg  10556  alephval2  10594  alephreg  10604  axextnd  10613  fpwwe2lem9  10661  pwfseq  10686  gch2  10697  axgroth3  10853  inaprc  10858  nlt1pi  10928  indpi  10929  1re  11243  mul02lem2  11420  addrid  11423  fimaxre  12194  fiminre  12197  supaddc  12217  supmul1  12219  inelr  12238  rimul  12239  nnge1  12276  zneo  12684  ltweuz  13984  hashrabsn1  14395  hashf1lem2  14477  hash2pwpr  14497  climuni  15570  fsum2d  15789  fsumabs  15819  fsumrlim  15829  fsumo1  15830  fsumiun  15839  fprod2d  15999  efne0  16115  ruclem13  16260  dvdslelem  16328  mod2eq1n2dvds  16366  nn0o1gt2  16400  divalglem0  16412  lcmfnnval  16643  prmreclem2  16937  prmreclem3  16938  mreexexd  17662  coaval  18084  xpcco  18198  pltirr  18349  frgpnabllem1  19859  ablfac1eulem  20060  prmgrpsimpgd  20102  mdetunilem9  22574  mretopd  23046  fiuncmp  23358  ptcmpfi  23767  filtop  23809  supnfcls  23974  flimfnfcls  23982  alexsubALTlem2  24002  alexsubALTlem4  24004  trust  24184  rectbntr0  24790  fsumcn  24830  ovoliunlem3  25475  ovolicc2lem4  25491  dyadmax  25569  vitali  25584  itgfsum  25798  dvmptfsum  25949  fta1g  26145  fta1  26286  aannenlem1  26306  aalioulem3  26312  logltb  26578  logdmn0  26618  ang180lem2  26789  angpined  26809  mumullem2  27159  lgsqrmodndvds  27333  gausslemma2dlem0i  27344  2lgs  27387  dchrisum0re  27493  chpdifbnd  27535  pntrlog2bnd  27564  pntibndlem3  27572  pnt3  27592  nofv  27638  nomaxmo  27679  nominmo  27680  noprc  27760  madebday  27874  addsproplem7  27944  negsproplem7  28002  elons2  28217  nbgrval  29281  vtxdginducedm1fi  29490  upgrewlkle2  29552  hiidge0  31045  chsupval  31282  chsupcl  31287  chsupss  31289  ococin  31355  chsupval2  31357  ssjo  31394  h1de2i  31500  pjss2i  31627  pjssmii  31628  sto2i  32184  stge1i  32185  stle0i  32186  stlei  32187  stlesi  32188  stm1i  32190  staddi  32193  stadd3i  32195  golem1  32218  stcltrlem1  32223  mdexchi  32282  chirred  32342  atabsi  32348  abrexdomjm  32454  iocinif  32722  cycpmcl  33075  elrgspnsubrunlem2  33191  voliune  34189  volfiniune  34190  probdif  34381  bnj849  34898  kur14lem9  35178  gonarlem  35358  gonar  35359  goalrlem  35360  goalr  35361  sscoid  35873  limsucncmpi  36405  bj-axc10  36743  bj-alequex  36744  bj-spimtv  36754  bj-moeub  36809  bj-exlimvmpi  36871  bj-exlimmpi  36872  bj-restpw  37052  bj-isrvec  37254  finxpreclem4  37354  domalom  37364  wl-isseteq  37465  wl-embant  37470  wl-orel12  37471  wl-euequf  37534  poimirlem9  37595  abrexdom  37696  heiborlem10  37786  dvrunz  37920  iss2  38304  equcomi1  38860  ax12eq  38901  ax12el  38902  ax12inda  38908  ax12v2-o  38909  cvrnrefN  39242  pmod1i  39809  pmodN  39811  osumcllem11N  39927  pexmidlem8N  39938  pl42lem3N  39942  cdleme18b  40253  dochexmidlem8  41428  imadomfi  41962  sticksstones3  42108  sn-axprlem3  42215  sn-exelALT  42216  sn-1ne2  42263  efne0d  42336  remul02  42398  sn-0tie0  42432  pellexlem3  42805  pell1234qrne0  42827  hbtlem6  43104  onsucelab  43238  omabs2  43307  nadd2rabex  43361  or3or  43998  isotone1  44023  isotone2  44024  clsf2  44101  ismnushort  44277  radcnvrat  44290  3impexpbicom  44457  sb5ALT  44502  eexinst01  44503  ax6e2eq  44534  sineq0ALT  44914  tcfr  44937  ssclaxsep  44956  omssaxinf2  44962  fzisoeu  45269  ovnsubaddlem2  46543  ormklocald  46846  natlocalincr  46848  tworepnotupword  46858  funressnfv  47013  faovcl  47170  sprsymrelfo  47442  clnbgrval  47767  cznnring  48136  zlmodzxznm  48372  elbigolo1  48436  dignn0flhalflem1  48494  nn0sumshdig  48502  rrx2xpref1o  48597  fonex  48727  vsetrec  49230