Theorem 3impib 1136

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Hypothesis

Ref	Expression
3impib.1	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Assertion

Ref	Expression
3impib	|- ( ( ph /\ ps /\ ch ) -> th )

Proof of Theorem 3impib

Step	Hyp	Ref	Expression
1		3impib.1	. . 3 |- ( ph -> ( ( ps /\ ch ) -> th ) )
2	1	expd 254	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1132	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  mob  2774  eqreu  2784  funimaexglem  5002  ssimaexg  5256  dfsmo2  5925  3ecoptocl  6218  distrnq0  6649  addassnq0  6652  uzind  8458  fzind  8462  fnn0ind  8463  xltnegi  8902  facwordi  9667  shftvalg  9724  shftval4g  9725  mulgcd  10405  coprmdvds1  10473  speano5  10739