Theorem imp31 254

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  imp41  350  imp5d  356  impl  377  anassrs  397  an31s  559  con4biddc  842  3imp  1175  3expa  1181  bilukdc  1374  reusv3  4381  dfimafn  5470  funimass4  5472  funimass3  5536  isopolem  5723  smores2  6191  tfrlem9  6216  nnmordi  6412  mulcanpig  7143  elnnz  9064  nzadd  9106  irradd  9438  irrmul  9439  uzsubsubfz  9827  fzo1fzo0n0  9960  elfzonelfzo  10007  tgcl  12233