Theorem imp41 286

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

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  adantlll 313  peano5 2394  fvco 2865  mapenlem1 3384  prlem936b 3948  nndiv 4453  uzwo 4605  nnwoOLD 4608  infxpidmlem11 4943  projlem28 5220  osumlem4 5533  spansncv 5542  sumdmdi 5785

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org