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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used by:  imp41  353  imp5d  359  impl  380  anassrs  404  an31s  576  con4biddc  869  3imp  1224  3expa  1234  bilukdc  1445  reusv3  4606  dfimafn  5751  funimass4  5753  funimass3  5825  dfimafnf  5955  isopolem  6028  suppfnss  6497  smores2  6565  tfrlem9  6590  nnmordi  6789  mulcanpig  7702  elnnz  9658  nzadd  9701  irradd  10055  irrmul  10057  uzsubsubfz  10462  fzo1fzo0n0  10605  elincfzoext  10621  elfzonelfzo  10658  swrdwrdsymbg  11450  wrd2ind  11509  infpnlem1  13158  tgcl  15214  uspgr2wlkeqi  16706  clwwlkext2edg  16761  clwwlknonex2lem2  16777