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  4400  fliftfund  5921  tfrlemibxssdm  6473  tfr1onlembxssdm  6489  tfrcllembxssdm  6502  imasmnd2  13485  grpinveu  13571  grpid  13572  grpasscan1  13596  imasgrp2  13647  imasrng  13919  imasring  14027  islmodd  14257  islssmd  14323  mulgghm2  14572  isxmetd  15021  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367