Theorem imp41 366

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

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  adantlll 396  adantllr 397  peano5 3241  oelim 4305  prlem936b 5308  lemul12a 5988  uzwo4OLD 6381  uzwo 6582  uzwoOLD 6583  cau3iri 7118  caucvglem4 7363  fsum0diag4 7466  infxpidmlem11 7774  iscncl 7980  xplmi 8184  cmsss 8208  bcthlem28 8237  grprcan 8280  grpinveu 8281  vacnlem3 8584  blocnilem 8719  projlem28 9489  osumlem4 9859  spansncvi 9875  sumdmdii 10624  usinuniop 11128  cmpmon 11270  2ndcctbss 11539  metdcn 11918  totbndbnd 12000

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 145  df-an 223

Copyright terms: Public domain