Theorem 3exp1 851

Description: Exportation from left triple conjunction.

Hypothesis

Ref	Expression
3exp1.1	|- (((ph /\ ps /\ ch) /\ th) -> ta)

Assertion

Ref	Expression
3exp1	|- (ph -> (ps -> (ch -> (th -> ta))))

Proof of Theorem 3exp1

Step	Hyp	Ref	Expression
1		3exp1.1	. . 3 |- (((ph /\ ps /\ ch) /\ th) -> ta)
2	1	ex 373	. 2 |- ((ph /\ ps /\ ch) -> (th -> ta))
3	2	3exp 834	1 |- (ph -> (ps -> (ch -> (th -> ta))))

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

This theorem is referenced by:  ltmpi 5043  qbtwnre 6279  sqlecant 6642  expcnvlem6 7232  blssex 7851  lmcvgnns 7940  pilem2 8667  strlem3a 10174  hstrlem3a 10182  irredlem1 10312  hmeomap 10504  hmeocna 10505  hmeocnb 10506  cnvhmphb 10512  cmpmon 10714  icmpmon 10715

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 779

Copyright terms: Public domain