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  1743  equs4v  2010  alequexv  2011  equcomiv  2025  equcomi  2028  equvinva  2041  aeveq  2065  spimt  2385  equs4  2415  axc15  2421  2ax6elem  2469  dfeumo  2537  mo4  2566  pm13.183  3562  sbcth  3694  sbcth2  3773  ssun3  4062  ssun4  4063  elpreqprlem  4748  uniintsn  4872  axprlem1  5287  axprlem2  5288  axprlem3  5289  axprlem4  5290  axprlem5  5291  axpr  5292  rext  5304  exss  5318  snopeqop  5360  propssopi  5362  uniopel  5370  opthhausdorff  5371  opthhausdorff0  5372  wefrc  5513  relopabi  5660  relop  5687  dmrnssfld  5807  iss  5871  sofld  6013  ordun  6267  funimass2  6416  fvbr0  6695  fvmptg  6767  funsndifnop  6917  fovcl  7288  ov3  7321  elovmpo  7400  limsssuc  7578  tfisi  7586  finds1  7625  frxp  7839  wfrlem5  7981  wfrlem16  7992  dfrecs3  8031  tfrlem1  8034  oaordi  8196  oaword2  8203  omeulem1  8232  oeworde  8243  oelim2  8245  nnaordi  8268  oaabs2  8296  0domg  8687  limenpsi  8735  dif1en  8754  enp1i  8823  findcard2OLD  8827  ordunifi  8835  fidomdm  8867  dffi3  8961  oismo  9070  wdom2d  9110  wdomima2g  9116  epnsym  9138  suc11reg  9148  elom3  9177  cantnfval2  9198  rankunb  9345  rankval4  9362  karden  9390  cardsn  9464  cardlim  9467  cardprclem  9474  fseqdom  9519  dfac12lem3  9638  kmlem2  9644  kmlem10  9652  cflim2  9756  cfslb2n  9761  fin23lem27  9821  fin23lem17  9831  axcc3  9931  axcc4  9932  acncc  9933  domtriomlem  9935  axdclem2  10013  imadomg  10027  alephval2  10065  alephreg  10075  axextnd  10084  fpwwe2lem9  10132  pwfseq  10157  gch2  10168  axgroth3  10324  inaprc  10329  nlt1pi  10399  indpi  10400  1re  10712  mul02lem2  10888  addid1  10891  fimaxre  11655  fiminre  11658  supaddc  11678  supmul1  11680  inelr  11699  rimul  11700  nnge1  11737  nnne0  11743  zneo  12139  ltweuz  13413  hashrabsn1  13820  hashf1lem2  13901  hash2pwpr  13921  climuni  14992  fsum2d  15212  fsumabs  15242  fsumrlim  15252  fsumo1  15253  fsumiun  15262  fprod2d  15420  efne0  15535  ruclem13  15680  dvdslelem  15747  mod2eq1n2dvds  15785  nn0o1gt2  15819  divalglem0  15831  lcmfnnval  16058  prmreclem2  16346  prmreclem3  16347  mreexexd  17015  coaval  17433  xpcco  17542  pltirr  17682  frgpnabllem1  19105  ablfac1eulem  19306  prmgrpsimpgd  19348  mdetunilem9  21364  mretopd  21836  fiuncmp  22148  ptcmpfi  22557  filtop  22599  supnfcls  22764  flimfnfcls  22772  alexsubALTlem2  22792  alexsubALTlem4  22794  trust  22974  rectbntr0  23577  fsumcn  23615  ovoliunlem3  24249  ovolicc2lem4  24265  dyadmax  24343  vitali  24358  itgfsum  24571  dvmptfsum  24719  fta1g  24912  fta1  25048  aannenlem1  25068  aalioulem3  25074  logltb  25335  logdmn0  25375  ang180lem2  25540  angpined  25560  mumullem2  25909  lgsqrmodndvds  26081  gausslemma2dlem0i  26092  2lgs  26135  dchrisum0re  26241  chpdifbnd  26283  pntrlog2bnd  26312  pntibndlem3  26320  pnt3  26340  nbgrval  27270  vtxdginducedm1fi  27478  upgrewlkle2  27540  hiidge0  29025  chsupval  29262  chsupcl  29267  chsupss  29269  ococin  29335  chsupval2  29337  ssjo  29374  h1de2i  29480  pjss2i  29607  pjssmii  29608  sto2i  30164  stge1i  30165  stle0i  30166  stlei  30167  stlesi  30168  stm1i  30170  staddi  30173  stadd3i  30175  golem1  30198  stcltrlem1  30203  mdexchi  30262  chirred  30322  atabsi  30328  abrexdomjm  30418  iocinif  30669  cycpmcl  30952  voliune  31759  volfiniune  31760  probdif  31949  bnj849  32468  kur14lem9  32739  gonarlem  32919  gonar  32920  goalrlem  32921  goalr  32922  dford5  33236  frxp2  33394  nofv  33493  nomaxmo  33534  nominmo  33535  noprc  33607  madebday  33710  no3indslem  33744  sscoid  33845  limsucncmpi  34264  bj-axc10  34585  bj-alequex  34586  bj-spimtv  34596  bj-moeub  34653  bj-exlimvmpi  34717  bj-exlimmpi  34718  bj-restpw  34873  finxpreclem4  35177  domalom  35187  wl-embant  35281  wl-orel12  35282  wl-euequf  35341  poimirlem9  35398  abrexdom  35500  heiborlem10  35590  dvrunz  35724  iss2  36091  equcomi1  36526  ax12eq  36567  ax12el  36568  ax12inda  36574  ax12v2-o  36575  cvrnrefN  36908  pmod1i  37474  pmodN  37476  osumcllem11N  37592  pexmidlem8N  37603  pl42lem3N  37607  cdleme18b  37918  dochexmidlem8  39093  sticksstones3  39699  sn-axprlem3  39761  sn-el  39762  sn-1ne2  39855  remul02  39949  sn-0tie0  39982  pellexlem3  40209  pell1234qrne0  40231  hbtlem6  40510  or3or  41161  isotone1  41188  isotone2  41189  clsf2  41266  radcnvrat  41454  3impexpbicom  41621  sb5ALT  41667  eexinst01  41668  ax6e2eq  41699  sineq0ALT  42079  fzisoeu  42361  ovnsubaddlem2  43635  funressnfv  44060  faovcl  44209  sprsymrelfo  44467  cznnring  45032  zlmodzxznm  45356  elbigolo1  45421  dignn0flhalflem1  45479  nn0sumshdig  45487  rrx2xpref1o  45582  vsetrec  45845