Theorem 3impib 1191

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

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

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 970

This theorem is referenced by:  mob  2908  eqreu  2918  funimaexglem  5271  ssimaexg  5548  rbropap  6211  dfsmo2  6255  3ecoptocl  6590  distrnq0  7400  addassnq0  7403  uzind  9302  fzind  9306  fnn0ind  9307  xltnegi  9771  facwordi  10653  shftvalg  10778  shftval4g  10779  mulgcd  11949  coprmdvds1  12023  pcfac  12280  mgmcl  12590  inopn  12641  basis1  12685  cnmpt2t  12933  cnmpt22  12934  cnmptcom  12938  xmeteq0  12999  sincosq1sgn  13387  sincosq2sgn  13388  sincosq3sgn  13389  sincosq4sgn  13390  speano5  13826