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  569  3expb  1231  reuss2  3505  reupick  3509  po2nr  4435  fvmptt  5774  fliftfund  5976  f1ocnv2d  6267  f1o3d  6271  addclpi  7658  addnidpig  7667  mulnqprl  7899  mulnqpru  7900  ltsubrp  10041  ltaddrp  10042  pfxccat3  11451  divgcdcoprm0  12823  infpnlem1  13082  imasmnd2  13707  imasgrp2  13863  imasrng  14195  imasring  14307  innei  15154  tgcnp  15200  isxmetd  15338  2lgslem1a1  16085