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  562  3expb  1199  reuss2  3407  reupick  3411  po2nr  4294  fvmptt  5587  fliftfund  5776  f1ocnv2d  6053  addclpi  7289  addnidpig  7298  mulnqprl  7530  mulnqpru  7531  ltsubrp  9647  ltaddrp  9648  divgcdcoprm0  12055  infpnlem1  12311  innei  12957  tgcnp  13003  isxmetd  13141