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  4608  dfimafn  5754  funimass4  5756  funimass3  5828  dfimafnf  5958  isopolem  6031  suppfnss  6501  smores2  6569  tfrlem9  6594  nnmordi  6793  mulcanpig  7708  elnnz  9665  nzadd  9708  irradd  10062  irrmul  10064  uzsubsubfz  10469  fzo1fzo0n0  10612  elincfzoext  10628  elfzonelfzo  10665  swrdwrdsymbg  11458  wrd2ind  11517  infpnlem1  13167  tgcl  15290  uspgr2wlkeqi  16813  clwwlkext2edg  16868  clwwlknonex2lem2  16884