Theorem imp32 363

Description: An importation inference.

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  imp42 369  anasss 440  ancom2s 487  ancom13s 488  3expb 833  reuss2 2273  reupick 2277  po2nr 2844  tz7.7 2970  onint 3003  isomin 3896  tfrlem5 3912  tz7.48lem 3952  oalimcl 4191  oaass 4192  omass 4208  oelim2 4219  en3d 4395  zorn2lem7 4781  addclpi 5007  addnidpi 5015  genpnnp 5095  genpnmax 5097  mulclprlem 5108  prlem936b 5141  lemul1itOLD 5808  peano2uz2 6163  uzwo3lem1 6178  uzwo3lem2 6179  elfz4t 6425  fsequb 6473  expwordit 6553  sqrlem6 6629  replimt 6713  seq1ublem 6877  bccl2t 6939  fsumcllem 6982  2climnn 7070  2climnn0 7071  climcmpc1 7108  isummulc1 7183  cvgratlem1ALT 7218  cvgratlem4 7224  infpnlem1 7485  tgss2t 7616  0ntr 7681  clsndisj 7685  neindisj 7710  innei 7715  islpi 7728  cnsscnp 7751  cncnpi 7752  cnconst 7759  opni2 7848  lmcvg 7915  lmnn 7918  metcnp4lem2 7952  metcn4i 7955  bcthlem21 8002  grpidinvlem3 8033  ubthlem13 8525  spansncol 9480  elspansn5t 9487  5oalem6 9595  lnopcon 9954  lnfncon 9981  nlelch 9985  leopmul2it 10059  mdit 10213  dmdit 10220  dmdsl3t 10233  atom1d 10271  cvexchlem 10286  atcvatlem 10303  irredlem3 10310  mdsymlem5 10325  cdj1 10351  nndivsub 10414  hmeogrp 10519  ltsubpostb 10578  ltaddpos2tb 10579  idmon 10695

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain