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  859  3imp  1196  3expa  1206  bilukdc  1416  reusv3  4525  dfimafn  5650  funimass4  5652  funimass3  5719  isopolem  5914  smores2  6403  tfrlem9  6428  nnmordi  6625  mulcanpig  7483  elnnz  9417  nzadd  9460  irradd  9802  irrmul  9803  uzsubsubfz  10204  fzo1fzo0n0  10344  elincfzoext  10359  elfzonelfzo  10396  swrdwrdsymbg  11155  wrd2ind  11214  infpnlem1  12797  tgcl  14651