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  1207  reuss2  3461  reupick  3465  po2nr  4374  fvmptt  5694  fliftfund  5889  f1ocnv2d  6173  addclpi  7475  addnidpig  7484  mulnqprl  7716  mulnqpru  7717  ltsubrp  9847  ltaddrp  9848  pfxccat3  11225  divgcdcoprm0  12538  infpnlem1  12797  imasmnd2  13399  imasgrp2  13561  imasrng  13833  imasring  13941  innei  14750  tgcnp  14796  isxmetd  14934  2lgslem1a1  15678