Theorem 3exp2 1252

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

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

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 1007

This theorem is referenced by:  3anassrs  1256  po2nr  4430  fliftfund  5970  tfrlemibxssdm  6558  tfr1onlembxssdm  6574  tfrcllembxssdm  6587  imasmnd2  13665  grpinveu  13751  grpid  13752  grpasscan1  13776  imasgrp2  13827  imasrng  14100  imasring  14208  islmodd  14441  islssmd  14507  mulgghm2  14756  isxmetd  15212  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558