Theorem 3impib 1179

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 256	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1175	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  mob  2866  eqreu  2876  funimaexglem  5206  ssimaexg  5483  rbropap  6140  dfsmo2  6184  3ecoptocl  6518  distrnq0  7267  addassnq0  7270  uzind  9162  fzind  9166  fnn0ind  9167  xltnegi  9618  facwordi  10486  shftvalg  10608  shftval4g  10609  mulgcd  11704  coprmdvds1  11772  inopn  12170  basis1  12214  cnmpt2t  12462  cnmpt22  12463  cnmptcom  12467  xmeteq0  12528  sincosq1sgn  12907  sincosq2sgn  12908  sincosq3sgn  12909  sincosq4sgn  12910  speano5  13142