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  3439  reupick  3443  po2nr  4340  fvmptt  5649  fliftfund  5840  f1ocnv2d  6122  addclpi  7387  addnidpig  7396  mulnqprl  7628  mulnqpru  7629  ltsubrp  9756  ltaddrp  9757  divgcdcoprm0  12239  infpnlem1  12497  imasgrp2  13180  imasrng  13452  imasring  13560  innei  14331  tgcnp  14377  isxmetd  14515