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

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

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