Theorem 3impib 1183

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

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

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 965

This theorem is referenced by:  mob  2894  eqreu  2904  funimaexglem  5253  ssimaexg  5530  rbropap  6190  dfsmo2  6234  3ecoptocl  6569  distrnq0  7379  addassnq0  7382  uzind  9275  fzind  9279  fnn0ind  9280  xltnegi  9739  facwordi  10614  shftvalg  10736  shftval4g  10737  mulgcd  11900  coprmdvds1  11968  inopn  12412  basis1  12456  cnmpt2t  12704  cnmpt22  12705  cnmptcom  12709  xmeteq0  12770  sincosq1sgn  13158  sincosq2sgn  13159  sincosq3sgn  13160  sincosq4sgn  13161  speano5  13530