Theorem imp41 368

Description: An importation inference.

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 350	. 2 |- ((ph /\ ps) -> (ch -> (th -> ta)))
3	2	imp31 362	1 |- ((((ph /\ ps) /\ ch) /\ th) -> ta)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  adantlll 396  adantllr 397  peano5 3148  oelim 4159  prlem936b 5134  lemul12it 5808  uzwo4OLD 6166  uzwo 6395  uzwoOLD 6396  cau3ir 6860  caucvglem4 7104  fsum0diag4 7204  infxpidmlem11 7513  iscncl 7720  xplmi 7923  cmsss 7947  bcthlem28 7976  grprcan 8013  grpinveu 8014  blocnilem 8408  projlem28 9152  osumlem4 9521  spansncv 9537  sumdmdi 10278  cmpmon 10621

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain