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	imp3a 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  589  impr  614  anasss  640  an13s  794  3expb  1181  reuss2  3618  reupick  3622  po2nr  4641  tz7.7  4732  ordtr2  4750  fvmptt  5777  fliftfund  5993  isomin  6015  f1ocnv2d  6300  onint  6395  tz7.48lem  6882  oalimcl  6987  oaass  6988  omass  7007  omabs  7074  finsschain  7606  infxpenlem  8168  axcc3  8595  zorn2lem7  8659  addclpi  9049  addnidpi  9058  genpnnp  9162  genpnmax  9164  mulclprlem  9176  dedekindle  9522  prodgt0  10162  ltsubrp  11010  ltaddrp  11011  swrdccatin1  12358  swrdccat3  12367  infpnlem1  13954  iscatd  14594  imasmnd2  15441  imasgrp2  15650  imasrng  16646  0ntr  18517  clsndisj  18521  innei  18571  islpi  18595  tgcnp  18699  haust1  18798  alexsublem  19458  alexsubb  19460  isxmetd  19743  axcontlem4  23036  grpoidinvlem3  23516  elspansn5  24800  5oalem6  24885  mdi  25522  dmdi  25529  dmdsl3  25542  atom1d  25580  cvexchlem  25595  atcvatlem  25612  chirredlem3  25619  mdsymlem5  25634  f1o3d  25772  dfon2lem6  27448  frmin  27550  soseq  27562  nodenselem5  27673  nodense  27677  broutsideof2  28000  outsideoftr  28007  outsideofeq  28008  nndivsub  28151  bddiblnc  28306  ftc1anc  28319  elicc3  28356  nn0prpwlem  28361  cntotbnd  28539  heiborlem6  28559  pridlc3  28717  wwlknimp  30167  wlkiswwlksur  30197  clwwlkf  30302  clwwlkextfrlem1  30515  bnj570  31621  leat2  32533  cvrexchlem  32657  cvratlem  32659  3dim2  32706  ps-2  32716  lncvrelatN  33019  osumcllem11N  33204