Theorem 3exp2 1256

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3anassrs  1260  po2nr  4454  fliftfund  6003  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  imasmnd2  13812  grpinveu  13896  grpid  13897  grpasscan1  13921  imasgrp2  13966  imasrng  14339  imasring  14453  islmodd  14713  islssmd  14780  mulgghm2  15027  isxmetd  15539  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885