Theorem 3exp2 1251

Description: Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)

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 115	. 2 |- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )
3	2	3expd 1250	1 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  3anassrs  1255  po2nr  4406  fliftfund  5938  tfrlemibxssdm  6493  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  imasmnd2  13553  grpinveu  13639  grpid  13640  grpasscan1  13664  imasgrp2  13715  imasrng  13988  imasring  14096  islmodd  14326  islssmd  14392  mulgghm2  14641  isxmetd  15090  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436