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  1188  reuss2  3625  reupick  3629  po2nr  4649  tz7.7  4740  ordtr2  4758  fvmptt  5784  fliftfund  6001  isomin  6023  f1ocnv2d  6306  onint  6401  tz7.48lem  6888  oalimcl  6991  oaass  6992  omass  7011  omabs  7078  finsschain  7610  infxpenlem  8172  axcc3  8599  zorn2lem7  8663  addclpi  9053  addnidpi  9062  genpnnp  9166  genpnmax  9168  mulclprlem  9180  dedekindle  9526  prodgt0  10166  ltsubrp  11014  ltaddrp  11015  swrdccatin1  12366  swrdccat3  12375  infpnlem1  13963  iscatd  14603  imasmnd2  15450  imasgrp2  15661  imasrng  16699  0ntr  18650  clsndisj  18654  innei  18704  islpi  18728  tgcnp  18832  haust1  18931  alexsublem  19591  alexsubb  19593  isxmetd  19876  axcontlem4  23164  grpoidinvlem3  23644  elspansn5  24928  5oalem6  25013  mdi  25650  dmdi  25657  dmdsl3  25670  atom1d  25708  cvexchlem  25723  atcvatlem  25740  chirredlem3  25747  mdsymlem5  25762  f1o3d  25899  dfon2lem6  27552  frmin  27654  soseq  27666  nodenselem5  27777  nodense  27781  broutsideof2  28104  outsideoftr  28111  outsideofeq  28112  nndivsub  28255  bddiblnc  28415  ftc1anc  28428  elicc3  28465  nn0prpwlem  28470  cntotbnd  28648  heiborlem6  28668  pridlc3  28826  wwlknimp  30274  wlkiswwlksur  30304  clwwlkf  30409  clwwlkextfrlem1  30622  dmatmul  30799  scmatmulcl  30809  scmatsgrp1  30812  bnj570  31785  leat2  32779  cvrexchlem  32903  cvratlem  32905  3dim2  32952  ps-2  32962  lncvrelatN  33265  osumcllem11N  33450