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

Theorem imp31 421
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 418 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
32imp 418 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  imp41  576  imp5d  582  impl  603  anassrs  629  an31s  781  3imp  1145  3expa  1151  pwssun  4299  fri  4355  ordelord  4414  tz7.7  4418  reusv3  4542  onint  4586  limsssuc  4641  tfindsg  4651  findsg  4683  dfimafn  5571  funimass4  5573  funimass3  5641  isomin  5834  isopolem  5842  smores2  6371  tfrlem1  6391  tfrlem9  6401  tz7.49  6457  oecl  6536  oaordi  6544  oaass  6559  omordi  6564  odi  6577  oen0  6584  nnaordi  6616  nnmordi  6629  php3  7047  domunfican  7129  dfac5  7755  cofsmo  7895  cfcoflem  7898  zorn2lem7  8129  tskwun  8406  mulcanpi  8524  ltexprlem7  8666  sup3  9711  elnnz  10034  irradd  10340  irrmul  10341  uzindi  11043  sqlecan  11209  unbenlem  12955  infpnlem1  12957  iscatd  13575  dirtr  14358  psrbaglefi  16118  isphld  16558  tgcl  16707  neindisj2  16860  2ndcdisj  17182  fgcl  17573  rnelfm  17648  alexsubALTlem3  17743  rngoueqz  21097  mdexchi  22915  atomli  22962  mdsymlem5  22987  sumdmdlem  22998  dfimafnf  23041  dfon2lem6  24144  predpo  24184  btwnconn1lem11  24720  trooo  25394  trinv  25395  ltrooo  25404  truni1  25505  osneisi  25531  cmptdst  25568  bwt2  25592  lvsovso  25626  supexr  25631  addidv2  25657  icccon2  25700  cmpmon  25815  icmpmon  25816  idsubfun  25858  eltintpar  25899  finminlem  26231  dmncan1  26701  eldioph2  26841  funressnfv  27991  dfaimafn  28027  nbcusgra  28159  cusgrauvtx  28168  frgra3vlem1  28178  3vfriswmgralem  28182  bnj517  28917  bnj1118  29014  lshpdisj  29177  2at0mat0  29714  llncvrlpln2  29746  lplncvrlvol2  29804  lhpexle2lem  30198  cdlemk33N  31098  cdlemk34  31099
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator