Theorem imp32 255

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

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem is referenced by:  imp42  351  impr  376  anasss  396  an13s  556  3expb  1182  reuss2  3351  reupick  3355  po2nr  4226  fvmptt  5505  fliftfund  5691  f1ocnv2d  5967  addclpi  7128  addnidpig  7137  mulnqprl  7369  mulnqpru  7370  ltsubrp  9471  ltaddrp  9472  divgcdcoprm0  11771  innei  12321  tgcnp  12367  isxmetd  12505