Theorem 3exp2 851

Description: Exportation from right triple conjunction.

Hypothesis

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

Assertion

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

Proof of Theorem 3exp2

Step	Hyp	Ref	Expression
1		3exp2.1	. . 3 |- ((ph /\ (ps /\ ch /\ th)) -> ta)
2	1	ex 373	. 2 |- (ph -> ((ps /\ ch /\ th) -> ta))
3	2	3expd 850	1 |- (ph -> (ps -> (ch -> (th -> ta))))

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

This theorem is referenced by:  po2nr 2847  cau3ir 6915  sncld 7787  bl2in 7843  lmuni 7951  xpcn 7976  grprcan 8063  grpinveu 8064  grpid 8065  grpasscan1 8077  hmeogrp 10538  cnfilca 10583  cnfilcaOLD 10584

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 777

Copyright terms: Public domain