Theorem imp32 434

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 432	. 2 |- ( ph -> ( ( ps /\ ch ) -> th ) )
3	2	imp 430	1 |- ( ( ph /\ ( ps /\ ch ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  imp42  597  impr  623  anasss  651  an13s  810  3expb  1206  reuss2  3753  reupick  3757  po2nr  4784  tz7.7  5465  ordtr2  5483  fvmptt  5978  fliftfund  6218  isomin  6240  f1ocnv2d  6531  onint  6633  tz7.48lem  7163  oalimcl  7266  oaass  7267  omass  7286  omabs  7353  finsschain  7884  infxpenlem  8446  axcc3  8869  zorn2lem7  8933  addclpi  9318  addnidpi  9327  genpnnp  9431  genpnmax  9433  mulclprlem  9445  dedekindle  9799  prodgt0  10451  ltsubrp  11336  ltaddrp  11337  swrdccatin1  12830  swrdccat3  12839  lcmfunsnlem2lem1  14599  infpnlem1  14842  prmgaplem4  15012  iscatd  15567  imasmnd2  16561  imasgrp2  16789  imasring  17835  mplcoe5lem  18679  dmatmul  19509  scmatmulcl  19530  scmatsgrp1  19534  smatvscl  19536  cpmatacl  19727  cpmatmcllem  19729  0ntr  20074  clsndisj  20078  innei  20128  islpi  20152  tgcnp  20256  haust1  20355  alexsublem  21046  alexsubb  21048  isxmetd  21328  axcontlem4  24984  wwlknimp  25401  wlkiswwlksur  25433  clwwlkf  25508  clwwlkextfrlem1  25790  grpoidinvlem3  25920  elspansn5  27213  5oalem6  27298  mdi  27934  dmdi  27941  dmdsl3  27954  atom1d  27992  cvexchlem  28007  atcvatlem  28024  chirredlem3  28031  mdsymlem5  28046  f1o3d  28219  bnj570  29712  dfon2lem6  30429  frmin  30475  soseq  30487  nodenselem5  30567  nodense  30571  broutsideof2  30882  outsideoftr  30889  outsideofeq  30890  elicc3  30966  nn0prpwlem  30971  nndivsub  31110  bddiblnc  31926  ftc1anc  31939  cntotbnd  32042  heiborlem6  32062  pridlc3  32220  leat2  32779  cvrexchlem  32903  cvratlem  32905  3dim2  32952  ps-2  32962  lncvrelatN  33265  osumcllem11N  33450  iccpartgt  38453  bgoldbachlt  38618  tgblthelfgott  38620  tgoldbach  38623  pfxccat3  38679  funcrngcsetcALT  39273