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  4356  fvmptt  5671  fliftfund  5866  f1ocnv2d  6150  addclpi  7440  addnidpig  7449  mulnqprl  7681  mulnqpru  7682  ltsubrp  9812  ltaddrp  9813  divgcdcoprm0  12423  infpnlem1  12682  imasmnd2  13284  imasgrp2  13446  imasrng  13718  imasring  13826  innei  14635  tgcnp  14681  isxmetd  14819  2lgslem1a1  15563