Theorem 3exp2 1228

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

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

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 983

This theorem is referenced by:  3anassrs  1232  po2nr  4356  fliftfund  5866  tfrlemibxssdm  6413  tfr1onlembxssdm  6429  tfrcllembxssdm  6442  imasmnd2  13284  grpinveu  13370  grpid  13371  grpasscan1  13395  imasgrp2  13446  imasrng  13718  imasring  13826  islmodd  14055  islssmd  14121  mulgghm2  14370  isxmetd  14819  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165