Theorem 3exp1 847

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 830	1 |- (ph -> (ps -> (ch -> (th -> ta))))

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

This theorem is referenced by:  ltmpi 5003  qbtwnre 6216  sqlecant 6572  expcnvlem6 7167  blssex 7794  lmcvgnns 7879  pilem2 8591  strlem3a 10089  hstrlem3a 10097  irredlem1 10225  hmeomap 10405  hmeocna 10406  hmeocnb 10407  cnvhmphb 10413  cmpmon 10585  icmpmon 10587

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