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  6570  tfrlem9  6595  nnmordi  6794  mulcanpig  7708  elnnz  9663  nzadd  9706  irradd  10061  irrmul  10063  uzsubsubfz  10468  fzo1fzo0n0  10611  elincfzoext  10627  elfzonelfzo  10664  swrdwrdsymbg  11457  wrd2ind  11516  infpnlem1  13166  tgcl  15307  uspgr2wlkeqi  16830  clwwlkext2edg  16885  clwwlknonex2lem2  16901