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  4454  fvmptt  5797  fliftfund  6003  f1ocnv2d  6294  f1o3d  6298  addclpi  7695  addnidpig  7704  mulnqprl  7936  mulnqpru  7937  ltsubrp  10102  ltaddrp  10103  pfxccat3  11522  divgcdcoprm0  12898  infpnlem1  13161  imasmnd2  13812  imasgrp2  13966  imasrng  14339  imasring  14453  innei  15355  tgcnp  15401  isxmetd  15539  2lgslem1a1  16371