Theorem 3exp2 1249

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

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

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 1004

This theorem is referenced by:  3anassrs  1253  po2nr  4402  fliftfund  5931  tfrlemibxssdm  6486  tfr1onlembxssdm  6502  tfrcllembxssdm  6515  imasmnd2  13522  grpinveu  13608  grpid  13609  grpasscan1  13633  imasgrp2  13684  imasrng  13956  imasring  14064  islmodd  14294  islssmd  14360  mulgghm2  14609  isxmetd  15058  dvidlemap  15402  dvidrelem  15403  dvidsslem  15404