Theorem 3exp2 1227

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980

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 982

This theorem is referenced by:  3anassrs  1231  po2nr  4341  fliftfund  5841  tfrlemibxssdm  6382  tfr1onlembxssdm  6398  tfrcllembxssdm  6411  grpinveu  13113  grpid  13114  grpasscan1  13138  imasgrp2  13183  imasrng  13455  imasring  13563  islmodd  13792  islssmd  13858  mulgghm2  14107  isxmetd  14526  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872