Theorem imp31 256

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
imp3.1	|- ( ph -> ( ps -> ( ch -> th ) ) )

Assertion

Ref	Expression
imp31	|- ( ( ( ph /\ ps ) /\ ch ) -> th )

Proof of Theorem imp31

Step	Hyp	Ref	Expression
1		imp3.1	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
2	1	imp 124	. 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:  imp41  353  imp5d  359  impl  380  anassrs  404  an31s  576  con4biddc  869  3imp  1224  3expa  1234  bilukdc  1445  reusv3  4606  dfimafn  5751  funimass4  5753  funimass3  5825  dfimafnf  5955  isopolem  6028  suppfnss  6497  smores2  6565  tfrlem9  6590  nnmordi  6789  mulcanpig  7703  elnnz  9659  nzadd  9702  irradd  10056  irrmul  10058  uzsubsubfz  10463  fzo1fzo0n0  10606  elincfzoext  10622  elfzonelfzo  10659  swrdwrdsymbg  11452  wrd2ind  11511  infpnlem1  13161  tgcl  15256  uspgr2wlkeqi  16774  clwwlkext2edg  16829  clwwlknonex2lem2  16845