MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpi Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 mpi.1 . . 3 𝜓
21a1i 11 . 2 (𝜑𝜓)
3 mpi.2 . 2 (𝜑 → (𝜓𝜒))
42, 3mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
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  694  mp3an3  1443  merco2  1730  equs4v  1999  alequexv  2000  equcomiv  2014  equcomi  2017  equvinva  2030  aeveq  2054  spsbeOLD  2082  spimt  2399  spimtOLD  2400  equs4  2434  axc15  2440  axc15OLD  2441  2ax6elem  2490  dfeumo  2617  mo4  2648  pm13.183  3663  pm13.183OLD  3664  sbcth  3791  sbcth2  3871  ssun3  4154  ssun4  4155  elpreqprlem  4795  uniintsn  4911  axprlem1  5320  axprlem2  5321  axprlem3  5322  axprlem4  5323  axprlem5  5324  axpr  5325  rext  5337  exss  5352  snopeqop  5393  propssopi  5395  uniopel  5403  opthhausdorff  5404  opthhausdorff0  5405  wefrc  5548  relopabi  5693  relop  5720  dmrnssfld  5840  iss  5902  sofld  6042  ordun  6290  funimass2  6434  fvbr0  6694  fvmptg  6763  funsndifnop  6909  fovcl  7269  ov3  7301  elovmpo  7380  limsssuc  7553  tfisi  7561  finds1  7599  frxp  7811  wfrlem5  7950  wfrlem16  7961  dfrecs3  8000  tfrlem1  8003  oaordi  8162  oaword2  8169  omeulem1  8198  oeworde  8209  oelim2  8211  nnaordi  8234  oaabs2  8262  0domg  8633  limenpsi  8681  enp1i  8742  findcard2  8747  ordunifi  8757  fidomdm  8790  dffi3  8884  oismo  8993  wdom2d  9033  wdomima2g  9039  epnsym  9061  suc11reg  9071  elom3  9100  cantnfval2  9121  rankunb  9268  rankval4  9285  karden  9313  cardsn  9387  cardlim  9390  cardprclem  9397  fseqdom  9441  dfac12lem3  9560  kmlem2  9566  kmlem10  9574  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  fimaxreOLD  11574  fiminre  11577  supaddc  11597  supmul1  11599  inelr  11617  rimul  11618  nnge1  11654  nnne0  11660  zneo  12054  ltweuz  13319  hashrabsn1  13725  hashf1lem2  13804  hash2pwpr  13824  climuni  14899  fsum2d  15116  fsumabs  15146  fsumrlim  15156  fsumo1  15157  fsumiun  15166  fprod2d  15325  efne0  15440  ruclem13  15585  dvdslelem  15649  mod2eq1n2dvds  15686  nn0o1gt2  15722  divalglem0  15734  lcmfnnval  15958  prmreclem2  16243  prmreclem3  16244  mreexexd  16909  coaval  17318  xpcco  17423  pltirr  17563  frgpnabllem1  18913  ablfac1eulem  19114  prmgrpsimpgd  19156  mdetunilem9  21145  mretopd  21616  fiuncmp  21928  ptcmpfi  22337  filtop  22379  supnfcls  22544  flimfnfcls  22552  alexsubALTlem2  22572  alexsubALTlem4  22574  trust  22753  rectbntr0  23355  fsumcn  23393  ovoliunlem3  24020  ovolicc2lem4  24036  dyadmax  24114  vitali  24129  itgfsum  24342  dvmptfsum  24487  fta1g  24676  fta1  24812  aannenlem1  24832  aalioulem3  24838  logltb  25096  logdmn0  25136  ang180lem2  25301  angpined  25321  mumullem2  25671  lgsqrmodndvds  25843  gausslemma2dlem0i  25854  2lgs  25897  dchrisum0re  26003  chpdifbnd  26045  pntrlog2bnd  26074  pntibndlem3  26082  pnt3  26102  nbgrval  27032  vtxdginducedm1fi  27240  upgrewlkle2  27302  hiidge0  28789  chsupval  29026  chsupcl  29031  chsupss  29033  ococin  29099  chsupval2  29101  ssjo  29138  h1de2i  29244  pjss2i  29371  pjssmii  29372  sto2i  29928  stge1i  29929  stle0i  29930  stlei  29931  stlesi  29932  stm1i  29934  staddi  29937  stadd3i  29939  golem1  29962  stcltrlem1  29967  mdexchi  30026  chirred  30086  atabsi  30092  abrexdomjm  30181  iocinif  30417  cycpmcl  30672  voliune  31374  volfiniune  31375  probdif  31564  bnj849  32083  kur14lem9  32345  gonarlem  32525  gonar  32526  goalrlem  32527  goalr  32528  dford5  32841  nofv  33048  nomaxmo  33085  noprc  33133  sscoid  33258  limsucncmpi  33677  bj-axc10  33989  bj-alequex  33990  bj-spimtv  34000  bj-moeub  34057  bj-exlimvmpi  34111  bj-exlimmpi  34112  bj-restpw  34264  finxpreclem4  34544  domalom  34554  wl-embant  34619  wl-orel12  34620  wl-euequf  34677  poimirlem9  34768  abrexdom  34873  heiborlem10  34966  dvrunz  35100  iss2  35469  equcomi1  35903  ax12eq  35944  ax12el  35945  ax12inda  35951  ax12v2-o  35952  cvrnrefN  36285  pmod1i  36851  pmodN  36853  osumcllem11N  36969  pexmidlem8N  36980  pl42lem3N  36984  cdleme18b  37295  dochexmidlem8  38470  sn-axprlem3  38974  sn-el  38975  sn-1ne2  39023  remul02  39100  pellexlem3  39293  pell1234qrne0  39315  hbtlem6  39594  or3or  40236  isotone1  40263  isotone2  40264  clsf2  40341  radcnvrat  40511  3impexpbicom  40678  sb5ALT  40724  eexinst01  40725  ax6e2eq  40756  sineq0ALT  41136  fzisoeu  41432  ovnsubaddlem2  42719  funressnfv  43144  faovcl  43265  sprsymrelfo  43491  cznnring  44059  zlmodzxznm  44384  elbigolo1  44449  dignn0flhalflem1  44507  nn0sumshdig  44515  rrx2xpref1o  44537  vsetrec  44637
  Copyright terms: Public domain W3C validator