Theorem imp42 620

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
imp4.1	|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Assertion

Ref	Expression
imp42	|- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ta )

Proof of Theorem imp42

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
2	1	imp32 449	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> ( th -> ta ) )
3	2	imp 445	1 |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ta )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  imp55  627  ltexprlem7  9864  iscatd  16334  isposd  16955  pospropd  17134  mulgghm2  19845  ordtbaslem  20992  txbas  21370  frgrncvvdeqlem8  27170  grporcan  27372  chirredlem1  29249  cvxpconn  31224  cvxsconn  31225  nocvxminlem  31893  rngonegmn1l  33740  prnc  33866