Theorem imp32 439

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

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  imp42  603  impr  629  anasss  657  an13s  817  3expb  1216  reuss2  3734  reupick  3738  po2nr  4786  tz7.7  5467  ordtr2  5485  fvmptt  5987  fliftfund  6230  isomin  6252  f1ocnv2d  6546  onint  6648  tz7.48lem  7183  oalimcl  7286  oaass  7287  omass  7306  omabs  7373  finsschain  7906  infxpenlem  8469  axcc3  8893  zorn2lem7  8957  addclpi  9342  addnidpi  9351  genpnnp  9455  genpnmax  9457  mulclprlem  9469  dedekindle  9823  prodgt0  10477  ltsubrp  11363  ltaddrp  11364  swrdccatin1  12875  swrdccat3  12884  lcmfunsnlem2lem1  14659  infpnlem1  14902  prmgaplem4  15072  iscatd  15627  imasmnd2  16621  imasgrp2  16849  imasring  17895  mplcoe5lem  18739  dmatmul  19570  scmatmulcl  19591  scmatsgrp1  19595  smatvscl  19597  cpmatacl  19788  cpmatmcllem  19790  0ntr  20135  clsndisj  20139  innei  20189  islpi  20213  tgcnp  20317  haust1  20416  alexsublem  21107  alexsubb  21109  isxmetd  21389  axcontlem4  25045  wwlknimp  25463  wlkiswwlksur  25495  clwwlkf  25570  clwwlkextfrlem1  25852  grpoidinvlem3  25982  elspansn5  27275  5oalem6  27360  mdi  27996  dmdi  28003  dmdsl3  28016  atom1d  28054  cvexchlem  28069  atcvatlem  28086  chirredlem3  28093  mdsymlem5  28108  f1o3d  28277  bnj570  29764  dfon2lem6  30482  frmin  30528  soseq  30540  nodenselem5  30622  nodense  30626  broutsideof2  30937  outsideoftr  30944  outsideofeq  30945  elicc3  31021  nn0prpwlem  31026  nndivsub  31165  bddiblnc  32056  ftc1anc  32069  cntotbnd  32172  heiborlem6  32192  pridlc3  32350  leat2  32904  cvrexchlem  33028  cvratlem  33030  3dim2  33077  ps-2  33087  lncvrelatN  33390  osumcllem11N  33575  iccpartgt  38778  bgoldbachlt  38943  tgblthelfgott  38945  tgoldbach  38948  pfxccat3  39006  ewlkle  39671  uhgr3cyclexlem  39921  funcrngcsetcALT  40273