Theorem imp31 252

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 122	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
3	2	imp 122	1 |- ( ( ( ph /\ ps ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  imp41  345  imp5d  351  impl  372  anassrs  392  an31s  534  con4biddc  787  3imp  1132  3expa  1138  bilukdc  1327  reusv3  4210  dfimafn  5243  funimass4  5245  funimass3  5304  isopolem  5481  smores2  5932  tfrlem9  5958  nnmordi  6112  mulcanpig  6525  elnnz  8361  nzadd  8403  irradd  8731  irrmul  8732  uzsubsubfz  9066  fzo1fzo0n0  9192  elfzonelfzo  9239