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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used by:  imp42  354  impr  379  anasss  403  an13s  573  3expb  1235  reuss2  3513  reupick  3517  po2nr  4456  fvmptt  5800  fliftfund  6006  f1ocnv2d  6297  f1o3d  6301  addclpi  7700  addnidpig  7709  mulnqprl  7941  mulnqpru  7942  ltsubrp  10107  ltaddrp  10108  pfxccat3  11527  divgcdcoprm0  12903  infpnlem1  13166  imasmnd2  13817  imasgrp2  13971  imasrng  14361  imasring  14477  innei  15406  tgcnp  15452  isxmetd  15590  2lgslem1a1  16427