Theorem imp32 281

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

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  imp42 287  anasss 337  3expb 613  reuss 1577  reupick 1578  po2nr 2135  wefrc 2195  tz7.7 2224  onint 2261  isomin 2937  tfrlem5 2953  tz7.48lem 2993  oalimcl 3162  oaass 3163  en3d 3304  zornlem7 3609  addclpi 3814  addnidpi 3822  genpnnp 3902  genpnmax 3904  mulclprlem 3915  prlem936b 3948  axrecex 4079  peano2uz 4602  uzwo3lem1 4614  uzwo3lem2 4615  qret 4631  sqrlem6 4736  replimt 4798  spansncol 5473  5oalem6 5549  atom1d 5750  cvexchlem 5759  atcvatlem 5770  mdsymlem5 5780

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org