Theorem imp32 257

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  imp42  354  impr  379  anasss  399  an13s  567  3expb  1206  reuss2  3443  reupick  3447  po2nr  4344  fvmptt  5653  fliftfund  5844  f1ocnv2d  6127  addclpi  7394  addnidpig  7403  mulnqprl  7635  mulnqpru  7636  ltsubrp  9765  ltaddrp  9766  divgcdcoprm0  12269  infpnlem1  12528  imasgrp2  13240  imasrng  13512  imasring  13620  innei  14399  tgcnp  14445  isxmetd  14583  2lgslem1a1  15327