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

Theorem imp32 422
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
imp3.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
imp32  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )

Proof of Theorem imp32
StepHypRef Expression
1 imp3.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21imp3a 420 . 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:  imp42  577  impr  602  anasss  628  an13s  778  3expb  1152  reuss2  3461  reupick  3465  po2nr  4343  tz7.7  4434  ordtr2  4452  onint  4602  fvmptt  5631  fliftfund  5828  isomin  5850  f1ocnv2d  6084  tfrlem5  6412  tz7.48lem  6469  oalimcl  6574  oaass  6575  omass  6594  omabs  6661  finsschain  7178  infxpenlem  7657  axcc3  8080  zorn2lem7  8145  addclpi  8532  addnidpi  8541  genpnnp  8645  genpnmax  8647  mulclprlem  8659  prodgt0  9617  ltsubrp  10401  ltaddrp  10402  infpnlem1  12973  iscatd  13591  joinle  14143  imasmnd2  14425  imasgrp2  14626  imasrng  15418  0ntr  16824  clsndisj  16828  innei  16878  islpi  16896  tgcnp  16999  haust1  17096  alexsublem  17754  alexsubb  17756  isxmetd  17907  grpoidinvlem3  20889  elspansn5  22169  5oalem6  22254  mdi  22891  dmdi  22898  dmdsl3  22911  atom1d  22949  cvexchlem  22964  atcvatlem  22981  chirredlem3  22988  mdsymlem5  23003  f1o3d  23053  dedekindle  24098  dfon2lem6  24215  frmin  24313  soseq  24325  nodenselem5  24410  nodense  24414  axcontlem4  24667  broutsideof2  24817  outsideoftr  24824  outsideofeq  24825  nndivsub  24968  bddiblnc  25021  islimrs4  25685  elicc3  26331  nn0prpwlem  26341  cntotbnd  26623  heiborlem6  26643  pridlc3  26801  bnj570  29253  leat2  30106  cvrexchlem  30230  cvratlem  30232  3dim2  30279  ps-2  30289  lncvrelatN  30592  osumcllem11N  30777
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