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  4496  dfimafn  5610  funimass4  5612  funimass3  5679  isopolem  5870  smores2  6354  tfrlem9  6379  nnmordi  6576  mulcanpig  7405  elnnz  9339  nzadd  9381  irradd  9723  irrmul  9724  uzsubsubfz  10125  fzo1fzo0n0  10262  elfzonelfzo  10309  infpnlem1  12539  tgcl  14326