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  590  imp5d  596  impl  617  anassrs  643  an31s  799  3imp  1176  3expa  1182  reusv3  4497  pwssun  4623  fri  4678  ordelord  4737  tz7.7  4741  dfimafn  5737  funimass4  5739  funimass3  5816  isomin  6025  isopolem  6033  onint  6405  limsssuc  6460  tfindsg  6470  findsg  6502  suppfnss  6713  smores2  6811  tfrlem9  6840  tz7.49  6896  oecl  6973  oaordi  6981  oaass  6996  omordi  7001  odi  7014  oen0  7021  nnaordi  7053  nnmordi  7066  php3  7493  domunfican  7580  dfac5  8294  cofsmo  8434  cfcoflem  8437  zorn2lem7  8667  tskwun  8947  mulcanpi  9065  ltexprlem7  9207  sup3  10283  elnnz  10652  uzletr  10865  irradd  10973  irrmul  10974  uzsubsubfz  11467  elfzonelfzo  11623  uzindi  11799  sqlecan  11968  swrdnd  12322  wrd2ind  12368  cshwlen  12432  cshwidxmod  12436  unbenlem  13965  infpnlem1  13967  iscatd  14607  dirtr  15402  psrbaglefi  17419  psrbaglefiOLD  17420  psgndiflemA  17990  isphld  18042  tgcl  18533  neindisj2  18686  bwthOLD  18973  2ndcdisj  19019  fgcl  19410  rnelfm  19485  alexsubALTlem3  19580  usgrares1  23258  usgrafis  23263  nbgraf1olem5  23289  nbcusgra  23306  cusgrares  23315  cusgrasize  23321  usgrnloop  23397  pthdepisspth  23408  fargshiftfva  23460  usgrcyclnl2  23462  eupatrl  23524  rngoueqz  23852  mdexchi  25674  atomli  25721  mdsymlem5  25746  sumdmdlem  25757  dfimafnf  25885  dfon2lem6  27530  predpo  27574  btwnconn1lem11  28057  itg2addnc  28371  finminlem  28438  dmncan1  28801  eldioph2  29025  funressnfv  29959  dfaimafn  29996  otiunsndisj  30057  otiunsndisjX  30058  uzuzle  30115  elfz2z  30123  usgra2wlkspth  30223  usgra2pthlem1  30225  usgra2adedgspthlem2  30229  el2spthonot  30314  2spontn0vne  30331  clwlkisclwwlklem2a  30372  clwwlkf1  30383  cshwlemma1  30414  clwlkfclwwlk  30442  wwlkextproplem2  30486  frgra3vlem1  30517  3vfriswmgralem  30521  vdgn0frgrav2  30542  vdgn1frgrav2  30544  frgrancvvdeqlemC  30557  frgrancvvdgeq  30561  frgrawopreglem5  30566  frg2woteq  30578  usg2spot2nb  30583  2spotmdisj  30586  extwwlkfablem2  30596  numclwwlkovf2ex  30604  scmatmulcl  30769  snlindsntor  30846  ldepspr  30848  bnj517  31712  bnj1118  31809  lshpdisj  32354  2at0mat0  32891  llncvrlpln2  32923  lplncvrlvol2  32981  lhpexle2lem  33375  cdlemk33N  34275  cdlemk34  34276
  Copyright terms: Public domain W3C validator