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  352  impr  377  anasss  397  an13s  557  3expb  1186  reuss2  3387  reupick  3391  po2nr  4269  fvmptt  5559  fliftfund  5747  f1ocnv2d  6024  addclpi  7247  addnidpig  7256  mulnqprl  7488  mulnqpru  7489  ltsubrp  9597  ltaddrp  9598  divgcdcoprm0  11978  innei  12574  tgcnp  12620  isxmetd  12758