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  1197  reuss2  3778  reupick  3782  po2nr  4813  tz7.7  4904  ordtr2  4922  fvmptt  5963  fliftfund  6197  isomin  6219  f1ocnv2d  6508  onint  6608  tz7.48lem  7103  oalimcl  7206  oaass  7207  omass  7226  omabs  7293  finsschain  7823  infxpenlem  8387  axcc3  8814  zorn2lem7  8878  addclpi  9266  addnidpi  9275  genpnnp  9379  genpnmax  9381  mulclprlem  9393  dedekindle  9740  prodgt0  10383  ltsubrp  11247  ltaddrp  11248  swrdccatin1  12667  swrdccat3  12676  infpnlem1  14283  iscatd  14924  imasmnd2  15771  imasgrp2  15985  imasrng  17052  mplcoe5lem  17901  dmatmul  18766  scmatmulcl  18787  scmatsgrp1  18791  smatvscl  18793  cpmatacl  18984  cpmatmcllem  18986  0ntr  19338  clsndisj  19342  innei  19392  islpi  19416  tgcnp  19520  haust1  19619  alexsublem  20279  alexsubb  20281  isxmetd  20564  axcontlem4  23946  wwlknimp  24363  wlkiswwlksur  24395  clwwlkf  24470  clwwlkextfrlem1  24753  grpoidinvlem3  24884  elspansn5  26168  5oalem6  26253  mdi  26890  dmdi  26897  dmdsl3  26910  atom1d  26948  cvexchlem  26963  atcvatlem  26980  chirredlem3  26987  mdsymlem5  27002  f1o3d  27144  dfon2lem6  28797  frmin  28899  soseq  28911  nodenselem5  29022  nodense  29026  broutsideof2  29349  outsideoftr  29356  outsideofeq  29357  nndivsub  29499  bddiblnc  29662  ftc1anc  29675  elicc3  29712  nn0prpwlem  29717  cntotbnd  29895  heiborlem6  29915  pridlc3  30073  bnj570  33042  leat2  34091  cvrexchlem  34215  cvratlem  34217  3dim2  34264  ps-2  34274  lncvrelatN  34577  osumcllem11N  34762