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  3453  reupick  3457  po2nr  4357  fvmptt  5673  fliftfund  5868  f1ocnv2d  6152  addclpi  7442  addnidpig  7451  mulnqprl  7683  mulnqpru  7684  ltsubrp  9814  ltaddrp  9815  divgcdcoprm0  12456  infpnlem1  12715  imasmnd2  13317  imasgrp2  13479  imasrng  13751  imasring  13859  innei  14668  tgcnp  14714  isxmetd  14852  2lgslem1a1  15596