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

Theorem imp31 434
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 431 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
32imp 431 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  imp41  597  imp5d  603  impl  625  anassrs  653  an31s  814  3imp  1200  3expa  1206  reusv3  4630  otiunsndisj  4724  pwssun  4757  fri  4813  predpo  5415  ordelord  5462  tz7.7  5466  dfimafn  5928  funimass4  5930  funimass3  6011  isomin  6241  isopolem  6249  onint  6634  limsssuc  6689  tfindsg  6699  findsg  6732  suppfnss  6949  smores2  7079  tfrlem9  7109  tz7.49  7168  oecl  7245  oaordi  7253  oaass  7268  omordi  7273  odi  7286  oen0  7293  nnaordi  7325  nnmordi  7338  php3  7762  domunfican  7848  dfac5  8561  cofsmo  8701  cfcoflem  8704  zorn2lem7  8934  tskwun  9211  mulcanpi  9327  ltexprlem7  9469  sup3  10568  elnnz  10949  irradd  11290  irrmul  11291  uzsubsubfz  11823  fzo1fzo0n0  11959  elincfzoext  11973  elfzonelfzo  12012  uzindi  12195  ssnn0fi  12198  sqlecan  12382  wrd2ind  12830  repswccat  12884  cshwlen  12897  cshwidxmod  12901  2cshwcshw  12920  lcmfunsnlem1  14603  lcmfdvdsb  14609  coprmprod  14671  unbenlem  14845  infpnlem1  14847  prmgaplem7  15020  iscatd  15572  initoeu1  15899  termoeu1  15906  dirtr  16475  telgsums  17616  psrbaglefi  18589  gsummoncoe1  18891  psgndiflemA  19161  isphld  19213  gsummatr01lem3  19674  cpmatmcllem  19734  mp2pm2mplem4  19825  chfacfisf  19870  chfacfisfcpmat  19871  cayleyhamilton1  19908  tgcl  19977  neindisj2  20131  2ndcdisj  20463  fgcl  20885  rnelfm  20960  alexsubALTlem3  21056  usgraexmpledg  25123  usgrares1  25130  usgrafis  25135  nbgraf1olem5  25165  nbcusgra  25183  cusgrares  25192  cusgrasize  25198  usgrwlknloop  25285  pthdepisspth  25296  usgra2adedgspthlem2  25332  usgra2wlkspth  25341  fargshiftfva  25359  usgrcyclnl2  25361  wwlkextinj  25450  wwlkextproplem2  25462  clwlkisclwwlklem2a  25505  clwlkisclwwlklem1  25507  clwwlkf1  25516  clwlkfclwwlk  25564  el2spthonot  25590  2spontn0vne  25607  eupatrl  25688  frgra3vlem1  25720  3vfriswmgralem  25724  vdgn0frgrav2  25744  vdgn1frgrav2  25746  frgrancvvdeqlemC  25759  frgrancvvdgeq  25763  frgrawopreglem5  25768  frg2woteq  25780  usg2spot2nb  25785  2spotmdisj  25788  extwwlkfablem2  25798  numclwwlkovf2ex  25806  rngoueqz  26150  mdexchi  27980  atomli  28027  mdsymlem5  28052  sumdmdlem  28063  dfimafnf  28229  bnj517  29698  bnj1118  29795  mclsind  30210  dfon2lem6  30435  btwnconn1lem11  30863  finminlem  30973  isbasisrelowllem1  31705  isbasisrelowllem2  31706  poimirlem27  31887  itg2addnc  31916  dmncan1  32229  lshpdisj  32478  2at0mat0  33015  llncvrlpln2  33047  lplncvrlvol2  33105  lhpexle2lem  33499  cdlemk33N  34401  cdlemk34  34402  eldioph2  35529  sge0iunmpt  38054  funressnfv  38348  dfaimafn  38385  iccelpart  38465  icceuelpart  38468  bgoldbtbndlem4  38621  otiunsndisjX  38714  elfz2z  38750  usgrexmpledg  38949  usgra2pthlem1  38971  zrtermorngc  39307  zrtermoringc  39376  snlindsntor  39570  ldepspr  39572  nn0sumshdiglemB  39737
  Copyright terms: Public domain W3C validator