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  10101  ltaddrp  10102  pfxccat3  11520  divgcdcoprm0  12895  infpnlem1  13158  imasmnd2  13808  imasgrp2  13962  imasrng  14304  imasring  14418  innei  15313  tgcnp  15359  isxmetd  15497  2lgslem1a1  16303