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  570  con4biddc  862  3imp  1217  3expa  1227  bilukdc  1438  reusv3  4551  dfimafn  5682  funimass4  5684  funimass3  5751  isopolem  5946  smores2  6440  tfrlem9  6465  nnmordi  6662  mulcanpig  7522  elnnz  9456  nzadd  9499  irradd  9841  irrmul  9842  uzsubsubfz  10243  fzo1fzo0n0  10383  elincfzoext  10399  elfzonelfzo  10436  swrdwrdsymbg  11196  wrd2ind  11255  infpnlem1  12882  tgcl  14738  uspgr2wlkeqi  16078