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

Theorem imp32 431
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 ) ) )
21impd 429 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
32imp 427 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  imp42  592  impr  617  anasss  645  an13s  801  3expb  1195  reuss2  3775  reupick  3779  po2nr  4802  tz7.7  4893  ordtr2  4911  fvmptt  5947  fliftfund  6186  isomin  6208  f1ocnv2d  6499  onint  6603  tz7.48lem  7098  oalimcl  7201  oaass  7202  omass  7221  omabs  7288  finsschain  7819  infxpenlem  8382  axcc3  8809  zorn2lem7  8873  addclpi  9259  addnidpi  9268  genpnnp  9372  genpnmax  9374  mulclprlem  9386  dedekindle  9734  prodgt0  10383  ltsubrp  11253  ltaddrp  11254  swrdccatin1  12702  swrdccat3  12711  infpnlem1  14515  iscatd  15165  imasmnd2  16159  imasgrp2  16387  imasring  17466  mplcoe5lem  18328  dmatmul  19169  scmatmulcl  19190  scmatsgrp1  19194  smatvscl  19196  cpmatacl  19387  cpmatmcllem  19389  0ntr  19742  clsndisj  19746  innei  19796  islpi  19820  tgcnp  19924  haust1  20023  alexsublem  20713  alexsubb  20715  isxmetd  20998  axcontlem4  24475  wwlknimp  24892  wlkiswwlksur  24924  clwwlkf  24999  clwwlkextfrlem1  25281  grpoidinvlem3  25409  elspansn5  26693  5oalem6  26778  mdi  27415  dmdi  27422  dmdsl3  27435  atom1d  27473  cvexchlem  27488  atcvatlem  27505  chirredlem3  27512  mdsymlem5  27527  f1o3d  27693  dfon2lem6  29463  frmin  29565  soseq  29577  nodenselem5  29688  nodense  29692  broutsideof2  30003  outsideoftr  30010  outsideofeq  30011  nndivsub  30153  bddiblnc  30328  ftc1anc  30341  elicc3  30378  nn0prpwlem  30383  cntotbnd  30535  heiborlem6  30555  pridlc3  30713  pfxccat3  32673  funcrngcsetcALT  33080  bnj570  34383  leat2  35435  cvrexchlem  35559  cvratlem  35561  3dim2  35608  ps-2  35618  lncvrelatN  35921  osumcllem11N  36106
  Copyright terms: Public domain W3C validator