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  565  con4biddc  852  3imp  1188  3expa  1198  bilukdc  1391  reusv3  4445  dfimafn  5545  funimass4  5547  funimass3  5612  isopolem  5801  smores2  6273  tfrlem9  6298  nnmordi  6495  mulcanpig  7297  elnnz  9222  nzadd  9264  irradd  9605  irrmul  9606  uzsubsubfz  10003  fzo1fzo0n0  10139  elfzonelfzo  10186  infpnlem1  12311  tgcl  12858