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  4412  fliftfund  5948  tfrlemibxssdm  6536  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  imasmnd2  13615  grpinveu  13701  grpid  13702  grpasscan1  13726  imasgrp2  13777  imasrng  14050  imasring  14158  islmodd  14389  islssmd  14455  mulgghm2  14704  isxmetd  15158  dvidlemap  15502  dvidrelem  15503  dvidsslem  15504