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

Theorem imp32 423
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 421 . 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:  imp42  578  impr  603  anasss  629  an13s  779  3expb  1154  reuss2  3564  reupick  3568  po2nr  4457  tz7.7  4548  ordtr2  4566  onint  4715  fvmptt  5759  fliftfund  5974  isomin  5996  f1ocnv2d  6234  tfrlem5  6577  tz7.48lem  6634  oalimcl  6739  oaass  6740  omass  6759  omabs  6826  finsschain  7348  infxpenlem  7828  axcc3  8251  zorn2lem7  8315  addclpi  8702  addnidpi  8711  genpnnp  8815  genpnmax  8817  mulclprlem  8829  prodgt0  9787  ltsubrp  10575  ltaddrp  10576  infpnlem1  13205  iscatd  13825  joinle  14377  imasmnd2  14659  imasgrp2  14860  imasrng  15652  0ntr  17058  clsndisj  17062  innei  17112  islpi  17135  tgcnp  17239  haust1  17338  alexsublem  17996  alexsubb  17998  isxmetd  18265  grpoidinvlem3  21642  elspansn5  22924  5oalem6  23009  mdi  23646  dmdi  23653  dmdsl3  23666  atom1d  23704  cvexchlem  23719  atcvatlem  23736  chirredlem3  23743  mdsymlem5  23758  f1o3d  23884  dedekindle  24967  dfon2lem6  25168  frmin  25266  soseq  25278  nodenselem5  25363  nodense  25367  axcontlem4  25620  broutsideof2  25770  outsideoftr  25777  outsideofeq  25778  nndivsub  25921  bddiblnc  25975  elicc3  26011  nn0prpwlem  26016  cntotbnd  26196  heiborlem6  26216  pridlc3  26374  bnj570  28614  leat2  29409  cvrexchlem  29533  cvratlem  29535  3dim2  29582  ps-2  29592  lncvrelatN  29895  osumcllem11N  30080
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