Theorem 3impib 1141

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 1137	1 |- ( ( ph /\ ps /\ ch ) -> th )

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

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 926

This theorem is referenced by:  mob  2797  eqreu  2807  funimaexglem  5097  ssimaexg  5366  dfsmo2  6052  3ecoptocl  6381  distrnq0  7018  addassnq0  7021  uzind  8857  fzind  8861  fnn0ind  8862  xltnegi  9297  facwordi  10148  shftvalg  10270  shftval4g  10271  mulgcd  11283  coprmdvds1  11351  inopn  11600  speano5  11839