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  4456  fliftfund  6006  tfrlemibxssdm  6603  tfr1onlembxssdm  6619  tfrcllembxssdm  6632  imasmnd2  13817  grpinveu  13901  grpid  13902  grpasscan1  13926  imasgrp2  13971  imasrng  14361  imasring  14477  islmodd  14737  islssmd  14804  mulgghm2  15051  isxmetd  15590  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936