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  2943  eqreu  2953  iotam  5247  funimaexglem  5338  ssimaexg  5620  rbropap  6298  dfsmo2  6342  3ecoptocl  6680  distrnq0  7521  addassnq0  7524  uzind  9431  fzind  9435  fnn0ind  9436  xltnegi  9904  facwordi  10814  shftvalg  10983  shftval4g  10984  mulgcd  12156  coprmdvds1  12232  pcfac  12491  mgmcl  12945  mhmlin  13042  mhmmulg  13236  issubg2m  13262  nsgbi  13277  srgmulgass  13488  dvdsrtr  13600  issubrng2  13709  issubrg2  13740  domnmuln0  13772  inopn  14182  basis1  14226  cnmpt2t  14472  cnmpt22  14473  cnmptcom  14477  xmeteq0  14538  sincosq1sgn  15002  sincosq2sgn  15003  sincosq3sgn  15004  sincosq4sgn  15005  speano5  15506