Theorem imp43 621

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

Hypothesis

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

Assertion

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

Proof of Theorem imp43

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
2	1	imp4b 613	. 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:  fundmen  8030  fiint  8237  ltexprlem6  9863  divgt0  10891  divge0  10892  le2sq2  12939  iscatd  16334  isfuncd  16525  islmodd  18869  lmodvsghm  18924  islssd  18936  basis2  20755  neindisj  20921  dvidlem  23679  spansneleq  28429  elspansn4  28432  adjmul  28951  kbass6  28980  mdsl0  29169  chirredlem1  29249  poimirlem29  33438  rngonegmn1r  33741  3dim1  34753  linepsubN  35038  pmapsub  35054  tgoldbach  41705  tgoldbachOLD  41712