Theorem 3impib 1203

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  mob  2946  eqreu  2956  iotam  5250  funimaexglem  5341  ssimaexg  5623  rbropap  6301  dfsmo2  6345  3ecoptocl  6683  distrnq0  7526  addassnq0  7529  uzind  9437  fzind  9441  fnn0ind  9442  xltnegi  9910  facwordi  10832  shftvalg  11001  shftval4g  11002  mulgcd  12183  coprmdvds1  12259  pcfac  12519  mgmcl  13002  mhmlin  13099  mhmmulg  13293  issubg2m  13319  nsgbi  13334  srgmulgass  13545  dvdsrtr  13657  issubrng2  13766  issubrg2  13797  domnmuln0  13829  inopn  14239  basis1  14283  cnmpt2t  14529  cnmpt22  14530  cnmptcom  14534  xmeteq0  14595  sincosq1sgn  15062  sincosq2sgn  15063  sincosq3sgn  15064  sincosq4sgn  15065  speano5  15590