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  13810  grpinveu  13894  grpid  13895  grpasscan1  13919  imasgrp2  13964  imasrng  14306  imasring  14420  islmodd  14680  islssmd  14747  mulgghm2  14994  isxmetd  15500  dvidlemap  15844  dvidrelem  15845  dvidsslem  15846