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  843  3imp  1176  3expa  1182  bilukdc  1375  reusv3  4414  dfimafn  5510  funimass4  5512  funimass3  5576  isopolem  5763  smores2  6231  tfrlem9  6256  nnmordi  6452  mulcanpig  7234  elnnz  9156  nzadd  9198  irradd  9533  irrmul  9534  uzsubsubfz  9927  fzo1fzo0n0  10060  elfzonelfzo  10107  tgcl  12403