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 )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is referenced by:  imp41  353  imp5d  359  impl  380  anassrs  400  an31s  572  con4biddc  865  3imp  1220  3expa  1230  bilukdc  1441  reusv3  4563  dfimafn  5703  funimass4  5705  funimass3  5772  isopolem  5973  suppfnss  6435  smores2  6503  tfrlem9  6528  nnmordi  6727  mulcanpig  7615  elnnz  9550  nzadd  9593  irradd  9941  irrmul  9942  uzsubsubfz  10344  fzo1fzo0n0  10485  elincfzoext  10501  elfzonelfzo  10538  swrdwrdsymbg  11311  wrd2ind  11370  infpnlem1  13012  tgcl  14875  uspgr2wlkeqi  16308  clwwlkext2edg  16363  clwwlknonex2lem2  16379