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  4315  fri  4371  ordelord  4430  tz7.7  4434  reusv3  4558  onint  4602  limsssuc  4657  tfindsg  4667  findsg  4699  dfimafn  5587  funimass4  5589  funimass3  5657  isomin  5850  isopolem  5858  smores2  6387  tfrlem1  6407  tfrlem9  6417  tz7.49  6473  oecl  6552  oaordi  6560  oaass  6575  omordi  6580  odi  6593  oen0  6600  nnaordi  6632  nnmordi  6645  php3  7063  domunfican  7145  dfac5  7771  cofsmo  7911  cfcoflem  7914  zorn2lem7  8145  tskwun  8422  mulcanpi  8540  ltexprlem7  8682  sup3  9727  elnnz  10050  irradd  10356  irrmul  10357  uzindi  11059  sqlecan  11225  unbenlem  12971  infpnlem1  12973  iscatd  13591  dirtr  14374  psrbaglefi  16134  isphld  16574  tgcl  16723  neindisj2  16876  2ndcdisj  17198  fgcl  17589  rnelfm  17664  alexsubALTlem3  17759  rngoueqz  21113  mdexchi  22931  atomli  22978  mdsymlem5  23003  sumdmdlem  23014  dfimafnf  23057  dfon2lem6  24215  predpo  24255  btwnconn1lem11  24792  itg2addnc  25005  trooo  25497  trinv  25498  ltrooo  25507  truni1  25608  osneisi  25634  cmptdst  25671  bwt2  25695  lvsovso  25729  supexr  25734  addidv2  25760  icccon2  25803  cmpmon  25918  icmpmon  25919  idsubfun  25961  eltintpar  26002  finminlem  26334  dmncan1  26804  eldioph2  26944  funressnfv  28096  dfaimafn  28133  nbcusgra  28298  cusgrauvtx  28309  usgrnloop  28351  pthdepisspth  28360  fargshiftfva  28384  eupatrl  28385  usgrcyclnl2  28387  frgra3vlem1  28424  3vfriswmgralem  28428  bnj517  29233  bnj1118  29330  lshpdisj  29799  2at0mat0  30336  llncvrlpln2  30368  lplncvrlvol2  30426  lhpexle2lem  30820  cdlemk33N  31720  cdlemk34  31721
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