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  3448  reupick  3452  po2nr  4327  tz7.7  4418  ordtr2  4436  onint  4586  fvmptt  5615  fliftfund  5812  isomin  5834  f1ocnv2d  6068  tfrlem5  6396  tz7.48lem  6453  oalimcl  6558  oaass  6559  omass  6578  omabs  6645  finsschain  7162  infxpenlem  7641  axcc3  8064  zorn2lem7  8129  addclpi  8516  addnidpi  8525  genpnnp  8629  genpnmax  8631  mulclprlem  8643  prodgt0  9601  ltsubrp  10385  ltaddrp  10386  infpnlem1  12957  iscatd  13575  joinle  14127  imasmnd2  14409  imasgrp2  14610  imasrng  15402  0ntr  16808  clsndisj  16812  innei  16862  islpi  16880  tgcnp  16983  haust1  17080  alexsublem  17738  alexsubb  17740  isxmetd  17891  grpoidinvlem3  20873  elspansn5  22153  5oalem6  22238  mdi  22875  dmdi  22882  dmdsl3  22895  atom1d  22933  cvexchlem  22948  atcvatlem  22965  chirredlem3  22972  mdsymlem5  22987  f1o3d  23037  dedekindle  24083  dfon2lem6  24144  frmin  24242  soseq  24254  nodenselem5  24339  nodense  24343  axcontlem4  24595  broutsideof2  24745  outsideoftr  24752  outsideofeq  24753  nndivsub  24896  islimrs4  25582  elicc3  26228  nn0prpwlem  26238  cntotbnd  26520  heiborlem6  26540  pridlc3  26698  bnj570  28937  leat2  29484  cvrexchlem  29608  cvratlem  29610  3dim2  29657  ps-2  29667  lncvrelatN  29970  osumcllem11N  30155
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