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  7694  addnidpig  7703  mulnqprl  7935  mulnqpru  7936  ltsubrp  10091  ltaddrp  10092  pfxccat3  11506  divgcdcoprm0  12879  infpnlem1  13138  imasmnd2  13759  imasgrp2  13913  imasrng  14255  imasring  14369  innei  15264  tgcnp  15310  isxmetd  15448  2lgslem1a1  16205