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  351  imp5d  357  impl  378  anassrs  398  an31s  560  con4biddc  847  3imp  1183  3expa  1193  bilukdc  1386  reusv3  4438  dfimafn  5535  funimass4  5537  funimass3  5601  isopolem  5790  smores2  6262  tfrlem9  6287  nnmordi  6484  mulcanpig  7276  elnnz  9201  nzadd  9243  irradd  9584  irrmul  9585  uzsubsubfz  9982  fzo1fzo0n0  10118  elfzonelfzo  10165  infpnlem1  12289  tgcl  12704