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  4374  fliftfund  5889  tfrlemibxssdm  6436  tfr1onlembxssdm  6452  tfrcllembxssdm  6465  imasmnd2  13399  grpinveu  13485  grpid  13486  grpasscan1  13510  imasgrp2  13561  imasrng  13833  imasring  13941  islmodd  14170  islssmd  14236  mulgghm2  14485  isxmetd  14934  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280