Theorem imp32 433

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

Step	Hyp	Ref	Expression
1		imp3.1	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
2	1	impd 431	. 2 |- ( ph -> ( ( ps /\ ch ) -> th ) )
3	2	imp 429	1 |- ( ( ph /\ ( ps /\ ch ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 369

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 371

This theorem is referenced by:  imp42  594  impr  619  anasss  647  an13s  801  3expb  1189  reuss2  3737  reupick  3741  po2nr  4761  tz7.7  4852  ordtr2  4870  fvmptt  5897  fliftfund  6114  isomin  6136  f1ocnv2d  6420  onint  6515  tz7.48lem  7005  oalimcl  7108  oaass  7109  omass  7128  omabs  7195  finsschain  7728  infxpenlem  8290  axcc3  8717  zorn2lem7  8781  addclpi  9171  addnidpi  9180  genpnnp  9284  genpnmax  9286  mulclprlem  9298  dedekindle  9644  prodgt0  10284  ltsubrp  11132  ltaddrp  11133  swrdccatin1  12491  swrdccat3  12500  infpnlem1  14088  iscatd  14729  imasmnd2  15576  imasgrp2  15788  imasrng  16833  mplcoe5lem  17670  0ntr  18806  clsndisj  18810  innei  18860  islpi  18884  tgcnp  18988  haust1  19087  alexsublem  19747  alexsubb  19749  isxmetd  20032  axcontlem4  23364  grpoidinvlem3  23844  elspansn5  25128  5oalem6  25213  mdi  25850  dmdi  25857  dmdsl3  25870  atom1d  25908  cvexchlem  25923  atcvatlem  25940  chirredlem3  25947  mdsymlem5  25962  f1o3d  26098  dfon2lem6  27744  frmin  27846  soseq  27858  nodenselem5  27969  nodense  27973  broutsideof2  28296  outsideoftr  28303  outsideofeq  28304  nndivsub  28446  bddiblnc  28609  ftc1anc  28622  elicc3  28659  nn0prpwlem  28664  cntotbnd  28842  heiborlem6  28862  pridlc3  29020  wwlknimp  30468  wlkiswwlksur  30498  clwwlkf  30603  clwwlkextfrlem1  30816  dmatmul  31041  scmatmulcl  31051  scmatsgrp1  31054  cpmatacl  31191  cpmatmcllem  31193  bnj570  32215  leat2  33262  cvrexchlem  33386  cvratlem  33388  3dim2  33435  ps-2  33445  lncvrelatN  33748  osumcllem11N  33933