MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imp31 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  4423  fri  4478  ordelord  4537  tz7.7  4541  reusv3  4664  onint  4708  limsssuc  4763  tfindsg  4773  findsg  4805  dfimafn  5707  funimass4  5709  funimass3  5778  isomin  5989  isopolem  5997  smores2  6545  tfrlem1  6565  tfrlem9  6575  tz7.49  6631  oecl  6710  oaordi  6718  oaass  6733  omordi  6738  odi  6751  oen0  6758  nnaordi  6790  nnmordi  6803  php3  7222  domunfican  7308  dfac5  7935  cofsmo  8075  cfcoflem  8078  zorn2lem7  8308  tskwun  8585  mulcanpi  8703  ltexprlem7  8845  sup3  9890  elnnz  10217  irradd  10523  irrmul  10524  uzindi  11240  sqlecan  11407  unbenlem  13196  infpnlem1  13198  iscatd  13818  dirtr  14601  psrbaglefi  16357  isphld  16801  tgcl  16950  neindisj2  17103  2ndcdisj  17433  fgcl  17824  rnelfm  17899  alexsubALTlem3  17994  usgrares1  21283  usgrafis  21288  nbgraf1olem5  21314  nbcusgra  21331  cusgrares  21340  cusgrasize  21346  usgrnloop  21412  pthdepisspth  21421  fargshiftfva  21467  usgrcyclnl2  21469  eupatrl  21531  rngoueqz  21859  mdexchi  23679  atomli  23726  mdsymlem5  23751  sumdmdlem  23762  dfimafnf  23879  dfon2lem6  25161  predpo  25201  btwnconn1lem11  25738  itg2addnc  25952  finminlem  26005  dmncan1  26370  eldioph2  26504  funressnfv  27654  dfaimafn  27691  frgra3vlem1  27746  3vfriswmgralem  27750  vdgn0frgrav2  27771  vdgn1frgrav2  27773  frgrancvvdeqlemC  27784  frgrancvvdgeq  27788  frgrawopreglem5  27793  bnj517  28587  bnj1118  28684  lshpdisj  29153  2at0mat0  29690  llncvrlpln2  29722  lplncvrlvol2  29780  lhpexle2lem  30174  cdlemk33N  31074  cdlemk34  31075
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