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

Theorem imp31 422
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 419 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
32imp 419 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  imp41  577  imp5d  583  impl  604  anassrs  630  an31s  782  3imp  1147  3expa  1153  pwssun  4482  fri  4537  ordelord  4596  tz7.7  4600  reusv3  4724  onint  4768  limsssuc  4823  tfindsg  4833  findsg  4865  dfimafn  5768  funimass4  5770  funimass3  5839  isomin  6050  isopolem  6058  smores2  6609  tfrlem1  6629  tfrlem9  6639  tz7.49  6695  oecl  6774  oaordi  6782  oaass  6797  omordi  6802  odi  6815  oen0  6822  nnaordi  6854  nnmordi  6867  php3  7286  domunfican  7372  dfac5  8002  cofsmo  8142  cfcoflem  8145  zorn2lem7  8375  tskwun  8652  mulcanpi  8770  ltexprlem7  8912  sup3  9958  elnnz  10285  irradd  10591  irrmul  10592  uzindi  11313  sqlecan  11480  unbenlem  13269  infpnlem1  13271  iscatd  13891  dirtr  14674  psrbaglefi  16430  isphld  16878  tgcl  17027  neindisj2  17180  bwth  17466  2ndcdisj  17512  fgcl  17903  rnelfm  17978  alexsubALTlem3  18073  usgrares1  21417  usgrafis  21422  nbgraf1olem5  21448  nbcusgra  21465  cusgrares  21474  cusgrasize  21480  usgrnloop  21556  pthdepisspth  21567  fargshiftfva  21619  usgrcyclnl2  21621  eupatrl  21683  rngoueqz  22011  mdexchi  23831  atomli  23878  mdsymlem5  23903  sumdmdlem  23914  dfimafnf  24036  dfon2lem6  25408  predpo  25452  btwnconn1lem11  26024  itg2addnc  26250  finminlem  26313  dmncan1  26678  eldioph2  26812  funressnfv  27960  dfaimafn  27997  otiunsndisj  28057  otiunsndisjX  28058  elfz2z  28090  elfzonelfzo  28116  swrdnd  28155  2cshw  28223  cshweqdif2s  28235  usgra2wlkspth  28262  usgra2pthlem1  28264  usgra2adedgspthlem2  28268  el2spthonot  28291  2spontn0vne  28308  frgra3vlem1  28328  3vfriswmgralem  28332  vdgn0frgrav2  28353  vdgn1frgrav2  28355  frgrancvvdeqlemC  28366  frgrancvvdgeq  28370  frgrawopreglem5  28375  frg2woteq  28387  usg2spot2nb  28392  2spotmdisj  28395  bnj517  29194  bnj1118  29291  lshpdisj  29723  2at0mat0  30260  llncvrlpln2  30292  lplncvrlvol2  30350  lhpexle2lem  30744  cdlemk33N  31644  cdlemk34  31645
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 178  df-an 361
  Copyright terms: Public domain W3C validator