Theorem imp31 256

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  imp41  353  imp5d  359  impl  380  anassrs  400  an31s  572  con4biddc  865  3imp  1220  3expa  1230  bilukdc  1441  reusv3  4586  dfimafn  5730  funimass4  5732  funimass3  5799  dfimafnf  5928  isopolem  6001  suppfnss  6470  smores2  6538  tfrlem9  6563  nnmordi  6762  mulcanpig  7666  elnnz  9604  nzadd  9647  irradd  9996  irrmul  9997  uzsubsubfz  10401  fzo1fzo0n0  10544  elincfzoext  10560  elfzonelfzo  10597  swrdwrdsymbg  11381  wrd2ind  11440  infpnlem1  13082  tgcl  15055  uspgr2wlkeqi  16488  clwwlkext2edg  16543  clwwlknonex2lem2  16559