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  1194  reuss2  3402  reupick  3406  po2nr  4287  fvmptt  5577  fliftfund  5765  f1ocnv2d  6042  addclpi  7268  addnidpig  7277  mulnqprl  7509  mulnqpru  7510  ltsubrp  9626  ltaddrp  9627  divgcdcoprm0  12033  infpnlem1  12289  innei  12803  tgcnp  12849  isxmetd  12987