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  570  con4biddc  858  3imp  1195  3expa  1205  bilukdc  1407  reusv3  4491  dfimafn  5605  funimass4  5607  funimass3  5674  isopolem  5865  smores2  6347  tfrlem9  6372  nnmordi  6569  mulcanpig  7395  elnnz  9327  nzadd  9369  irradd  9711  irrmul  9712  uzsubsubfz  10113  fzo1fzo0n0  10250  elfzonelfzo  10297  infpnlem1  12497  tgcl  14232