Theorem imp41 619

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

Hypothesis

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

Assertion

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

Proof of Theorem imp41

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
2	1	imp 445	. 2 |- ( ( ph /\ ps ) -> ( ch -> ( th -> ta ) ) )
3	2	imp31 448	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:  3anassrs  1290  ad4ant13  1292  ad4ant14  1293  ad4ant123  1294  ad4ant124  1295  ad4ant134  1296  ad4ant23  1297  ad4ant24  1298  ad4ant234  1299  ad5ant13  1301  ad5ant14  1302  ad5ant15  1303  ad5ant23  1304  ad5ant24  1305  ad5ant25  1306  ad5ant245  1307  ad5ant234  1308  ad5ant235  1309  ad5ant123  1310  ad5ant124  1311  ad5ant125  1312  ad5ant134  1313  ad5ant135  1314  ad5ant145  1315  ad5ant2345  1317  peano5  7089  oelim  7614  lemul12a  10881  uzwo  11751  elfznelfzo  12573  injresinj  12589  swrdswrd  13460  2cshwcshw  13571  dvdsprmpweqle  15590  catidd  16341  grpinveu  17456  2ndcctbss  21258  rusgrnumwwlks  26869  erclwwlkstr  26936  erclwwlksntr  26948  grpoinveu  27373  spansncvi  28511  sumdmdii  29274  relowlpssretop  33212  matunitlindflem1  33405  unichnidl  33830  linepsubN  35038  pmapsub  35054  cdlemkid4  36222  hbtlem2  37694  ply1mulgsumlem2  42175