Theorem imp32 423

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

Syntax hints:   -> wi 4   /\ wa 359

This theorem is referenced by:  imp42  578  impr  603  anasss  629  an13s  779  3expb  1154  reuss2  3581  reupick  3585  po2nr  4476  tz7.7  4567  ordtr2  4585  onint  4734  fvmptt  5779  fliftfund  5994  isomin  6016  f1ocnv2d  6254  tfrlem5  6600  tz7.48lem  6657  oalimcl  6762  oaass  6763  omass  6782  omabs  6849  finsschain  7371  infxpenlem  7851  axcc3  8274  zorn2lem7  8338  addclpi  8725  addnidpi  8734  genpnnp  8838  genpnmax  8840  mulclprlem  8852  prodgt0  9811  ltsubrp  10599  ltaddrp  10600  infpnlem1  13233  iscatd  13853  joinle  14405  imasmnd2  14687  imasgrp2  14888  imasrng  15680  0ntr  17090  clsndisj  17094  innei  17144  islpi  17167  tgcnp  17271  haust1  17370  alexsublem  18028  alexsubb  18030  isxmetd  18309  grpoidinvlem3  21747  elspansn5  23029  5oalem6  23114  mdi  23751  dmdi  23758  dmdsl3  23771  atom1d  23809  cvexchlem  23824  atcvatlem  23841  chirredlem3  23848  mdsymlem5  23863  f1o3d  23994  dedekindle  25141  dfon2lem6  25358  frmin  25456  soseq  25468  nodenselem5  25553  nodense  25557  axcontlem4  25810  broutsideof2  25960  outsideoftr  25967  outsideofeq  25968  nndivsub  26111  bddiblnc  26174  elicc3  26210  nn0prpwlem  26215  cntotbnd  26395  heiborlem6  26415  pridlc3  26573  swrdccatin1  28016  bnj570  28982  leat2  29777  cvrexchlem  29901  cvratlem  29903  3dim2  29950  ps-2  29960  lncvrelatN  30263  osumcllem11N  30448

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361