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  535  con4biddc  788  3imp  1133  3expa  1139  bilukdc  1328  reusv3  4218  dfimafn  5254  funimass4  5256  funimass3  5315  isopolem  5492  smores2  5943  tfrlem9  5968  nnmordi  6155  mulcanpig  6587  elnnz  8442  nzadd  8484  irradd  8812  irrmul  8813  uzsubsubfz  9142  fzo1fzo0n0  9269  elfzonelfzo  9316