Theorem 3imp1 845

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

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

This theorem is referenced by:  fvco 3765  divasst 5712  lemul1it 5801  divexpt 6538  expmwordit 6545  expnbndt 6593  expcnvlem6 7175  cnpco 7719  cnconst 7730  bl2in 7795  lmuni 7902  nvcnpi4 8368  homco1t 9667  homulasst 9668  hoadddirt 9670  homco2t 9840  and4as 10368  and4com 10369  11st22nd 10390

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 776

Copyright terms: Public domain