Theorem 3imp1 844

Description: Importation to left triple conjunction.

Hypothesis

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

Assertion

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

Proof of Theorem 3imp1

Step	Hyp	Ref	Expression
1		3imp1.1	. . 3 |- (ph -> (ps -> (ch -> (th -> ta))))
2	1	3imp 825	. 2 |- ((ph /\ ps /\ ch) -> (th -> ta))
3	2	imp 350	1 |- (((ph /\ ps /\ ch) /\ th) -> ta)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 773

This theorem is referenced by:  fvco 3759  divasst 5704  lemul1it 5793  divexpt 6530  expmwordit 6537  expnbndt 6585  expcnvlem6 7167  cnpco 7708  cnconst 7719  bl2in 7783  lmuni 7886  nvcnpi4 8355  homco1t 9644  homulasst 9645  hoadddirt 9647  homco2t 9817  and4as 10332  and4com 10333  11st22nd 10354

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  df-3an 775

Copyright terms: Public domain