Theorem mpi 21

Description: A nested modus ponens inference. Inference associated with com12 33. (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 16	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mpisyl  22  syl6mpi  68  mp2ani  711  mp3an3  1479  merco2  1768  equs4v  2034  alequexv  2035  equcomiv  2048  equcomi  2051  equvinva  2064  aeveq  2092  spimt  2418  equs4  2448  axc15  2454  2ax6elem  2502  dfeumo  2564  mo4  2594  sbcth  3757  sbcth2  3835  ssun3  4181  ssun4  4182  vn0  4294  elpreqprlem  4824  uniintsn  4948  sepexlem  5257  axprlem2  5390  axprlem4  5392  axpr  5393  axprlem1OLD  5394  axprglem  5398  exel  5406  rext  5420  exss  5435  snopeqop  5482  propssopi  5484  uniopel  5493  opthhausdorff  5494  opthhausdorff0  5495  wefrc  5649  relopabi  5805  relop  5833  dmrnssfld  5961  iss  6033  sofld  6185  ordun  6476  funimass2  6634  fvbr0  6923  fvmptg  7002  funsndifnop  7166  ov3  7593  elovmpo  7676  dford5  7808  limsssuc  7871  tfisi  7880  finds1  7921  frxp  8151  frxp2  8174  frxp3  8181  dfrecs3  8394  tfrlem1  8397  oaordi  8568  oaword2  8575  omeulem1  8604  oeworde  8616  oelim2  8618  nnaordi  8641  oaabs2  8672  limenpsi  9185  dif1en  9191  ordunifi  9295  fidomdm  9337  dffi3  9436  oismo  9547  wdom2d  9587  wdomima2g  9593  epnsym  9623  suc11reg  9633  elom3  9662  cantnfval2  9683  rankunb  9877  rankval4  9897  karden  9972  kardenOLD  9973  cardsn  10063  cardlim  10066  cardprclem  10073  fseqdom  10118  dfac12lem3  10237  kmlem2  10243  kmlem10  10251  cflim2  10354  cfslb2n  10359  fin23lem27  10419  fin23lem17  10429  axcc3  10529  axcc4  10530  acncc  10531  domtriomlem  10533  axdclem2  10611  imadomg  10626  imadomnum  10627  alephval2  10670  alephreg  10680  axextnd  10689  fpwwe2lem9  10737  pwfseq  10762  gch2  10773  axgroth3  10929  inaprc  10934  nlt1pi  11004  indpi  11005  1re  11321  mul02lem2  11500  addrid  11503  fimaxre  12274  fiminre  12277  supaddc  12297  supmul1  12299  rimul  12324  nnge1  12379  zneo  12795  ltweuz  14117  hashrabsn1  14531  hashf1lem2  14614  hash2pwpr  14634  climuni  15734  fsum2d  15952  fsumabs  15983  fsumrlim  15993  fsumo1  15994  fsumiun  16003  fprod2d  16163  efne0d  16278  efne0OLD  16280  ruclem13  16425  dvdslelem  16494  mod2eq1n2dvds  16532  nn0o1gt2  16566  divalglem0  16578  lcmfnnval  16814  prmreclem2  17110  prmreclem3  17111  mreexexd  17837  coaval  18258  xpcco  18372  pltirr  18522  frgpnabllem1  20102  ablfac1eulem  20303  prmgrpsimpgd  20345  mdetunilem9  22950  mretopd  23425  fiuncmp  23737  ptcmpfi  24147  filtop  24189  supnfcls  24354  flimfnfcls  24362  alexsubALTlem2  24382  alexsubALTlem4  24384  trust  24563  rectbntr0  25167  fsumcn  25206  ovoliunlem3  25840  ovolicc2lem4  25856  dyadmax  25934  vitali  25949  itgfsum  26162  dvmptfsum  26310  fta1g  26503  fta1  26644  aannenlem1  26670  aalioulem3  26676  logltb  26943  logdmn0  26983  ang180lem2  27153  angpined  27173  mumullem2  27522  lgsqrmodndvds  27695  gausslemma2dlem0i  27706  2lgs  27749  dchrisum0re  27855  chpdifbnd  27897  pntrlog2bnd  27926  pntibndlem3  27934  pnt3  27954  nofv  28029  nomaxmo  28070  nominmo  28071  noprc  28157  madebday  28301  addsproplem7  28376  negsproplem7  28435  elons2  28659  nbgrval  29932  vtxdginducedm1fi  30140  upgrewlkle2  30202  hiidge0  31715  chsupval  31952  chsupcl  31957  chsupss  31959  ococin  32025  chsupval2  32027  ssjo  32064  h1de2i  32170  pjss2i  32297  pjssmii  32298  sto2i  32854  stge1i  32855  stle0i  32856  stlei  32857  stlesi  32858  stm1i  32860  staddi  32863  stadd3i  32865  golem1  32888  stcltrlem1  32893  mdexchi  32952  chirred  33012  atabsi  33018  abrexdomjm  33160  iocinif  33429  cycpmcl  33733  elrgspnsubrunlem2  33865  voliune  34918  volfiniune  34919  probdif  35108  bnj849  35611  axprALT2  35798  acwer1prclem  35833  acwer1prc  35834  j0ltaleph  35965  dfk12  35969  dfk22  35970  dfk32  35971  onvf1odlem4  35991  onvf1od  35992  vonf1onprcf1ac  36001  onvfowev  36007  kur14lem9  36103  gonarlem  36283  gonar  36284  goalrlem  36285  goalr  36286  sscoid  36805  limsucncmpi  37363  axtco1from2  37393  axtcond  37396  bj-nnf-spime  37807  bj-axc10  37825  bj-alequex  37826  bj-spimtv  37836  bj-moeub  37891  bj-exlimvmpi  37953  bj-exlimmpi  37954  bj-restpw  38155  bj-isrvec  38358  finxpreclem4  38460  domalom  38470  wl-isseteq  38571  wl-embant  38585  wl-orel12  38586  wl-euequf  38649  poimirlem9  38690  dfprop2  38789  abrexdom  38807  heiborlem10  38897  dvrunz  39031  iss2  39419  equcomi1  40100  ax12eq  40141  ax12el  40142  ax12inda  40148  ax12v2-o  40149  cvrnrefN  40482  pmod1i  41048  pmodN  41050  osumcllem11N  41166  pexmidlem8N  41177  pl42lem3N  41181  cdleme18b  41492  dochexmidlem8  42667  imadomfi  43195  sticksstones3  43341  sn-axprlem3  43415  sn-exelALT  43416  sn-1ne2  43473  remul02  43599  sn-0tie0  43658  pellexlem3  43981  pell1234qrne0  44003  hbtlem6  44274  onsucelab  44408  omabs2  44477  nadd2rabex  44531  or3or  45166  isotone1  45191  isotone2  45192  clsf2  45269  ismnushort  45428  radcnvrat  45441  3impexpbicom  45605  sb5ALT  45650  eexinst01  45651  ax6e2eq  45682  sineq0ALT  46061  tcfr  46095  ssclaxsep  46114  omssaxinf2  46120  nregmodel  46149  fzisoeu  46458  ovnsubaddlem2  47723  ormklocald  48028  funressnfv  48255  faovcl  48412  sprsymrelfo  48721  clnbgrval  49062  gpgedgiov  49305  gpgedg2ov  49306  gpgedg2iv  49307  pgnioedg1  49348  pgnioedg2  49349  pgnioedg3  49350  pgnioedg4  49351  pgnioedg5  49352  pgnbgreunbgrlem2lem1  49354  pgnbgreunbgrlem2lem2  49355  pgnbgreunbgrlem2lem3  49356  pgnbgreunbgrlem5lem1  49360  pgnbgreunbgrlem5lem2  49361  cznnring  49501  zlmodzxznm  49751  elbigolo1  49811  dignn0flhalflem1  49869  nn0sumshdig  49877  fonex  50120  vsetrec  51013