MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imp31 Structured version   Unicode version

Theorem imp31 432
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
imp3.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
imp31  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )

Proof of Theorem imp31
StepHypRef Expression
1 imp3.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21imp 429 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
32imp 429 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  imp41  593  imp5d  599  impl  620  anassrs  648  an31s  804  3imp  1190  3expa  1196  reusv3  4655  otiunsndisj  4753  pwssun  4786  fri  4841  ordelord  4900  tz7.7  4904  dfimafn  5915  funimass4  5917  funimass3  5996  isomin  6220  isopolem  6228  onint  6609  limsssuc  6664  tfindsg  6674  findsg  6706  suppfnss  6925  smores2  7025  tfrlem9  7054  tz7.49  7110  oecl  7187  oaordi  7195  oaass  7210  omordi  7215  odi  7228  oen0  7235  nnaordi  7267  nnmordi  7280  php3  7703  domunfican  7792  dfac5  8508  cofsmo  8648  cfcoflem  8651  zorn2lem7  8881  tskwun  9161  mulcanpi  9277  ltexprlem7  9419  sup3  10499  elnnz  10873  irradd  11205  irrmul  11206  uzsubsubfz  11706  elfzonelfzo  11879  uzindi  12058  ssnn0fi  12061  sqlecan  12241  swrdnd  12619  wrd2ind  12665  cshwlen  12732  cshwidxmod  12736  2cshwcshw  12755  unbenlem  14284  infpnlem1  14286  iscatd  14927  dirtr  15722  telgsums  16822  psrbaglefi  17810  psrbaglefiOLD  17811  gsummoncoe1  18133  psgndiflemA  18420  isphld  18472  cpmatmcllem  19002  mp2pm2mplem4  19093  chfacfisf  19138  chfacfisfcpmat  19139  cayleyhamilton1  19176  tgcl  19253  neindisj2  19406  bwthOLD  19693  2ndcdisj  19739  fgcl  20130  rnelfm  20205  alexsubALTlem3  20300  usgraexmpledg  24095  usgrares1  24102  usgrafis  24107  nbgraf1olem5  24137  nbcusgra  24155  cusgrares  24164  cusgrasize  24170  usgrnloop  24257  pthdepisspth  24268  usgra2adedgspthlem2  24304  usgra2wlkspth  24313  fargshiftfva  24331  usgrcyclnl2  24333  wwlkextproplem2  24434  clwlkisclwwlklem2a  24477  clwlkisclwwlklem1  24479  clwwlkf1  24488  clwlkfclwwlk  24536  el2spthonot  24562  2spontn0vne  24579  eupatrl  24660  frgra3vlem1  24692  3vfriswmgralem  24696  vdgn0frgrav2  24717  vdgn1frgrav2  24719  frgrancvvdeqlemC  24732  frgrancvvdgeq  24736  frgrawopreglem5  24741  frg2woteq  24753  usg2spot2nb  24758  2spotmdisj  24761  extwwlkfablem2  24771  numclwwlkovf2ex  24779  rngoueqz  25124  mdexchi  26946  atomli  26993  mdsymlem5  27018  sumdmdlem  27029  dfimafnf  27162  dfon2lem6  28813  predpo  28857  btwnconn1lem11  29340  itg2addnc  29662  finminlem  29729  dmncan1  30092  eldioph2  30315  funressnfv  31696  dfaimafn  31733  otiunsndisjX  31784  elfz2z  31814  usgra2pthlem1  31836  snlindsntor  32162  ldepspr  32164  bnj517  33031  bnj1118  33128  lshpdisj  33793  2at0mat0  34330  llncvrlpln2  34362  lplncvrlvol2  34420  lhpexle2lem  34814  cdlemk33N  35714  cdlemk34  35715
  Copyright terms: Public domain W3C validator