Theorem 3impib 1228

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

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

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 1007

This theorem is referenced by:  mob  3002  eqreu  3012  iotam  5349  funimaexglem  5444  ssimaexg  5744  funopdmsn  5869  rbropap  6487  dfsmo2  6531  3ecoptocl  6871  distrnq0  7790  addassnq0  7793  uzind  9707  fzind  9711  fnn0ind  9712  xltnegi  10187  facwordi  11127  shftvalg  11546  shftval4g  11547  mulgcd  12737  coprmdvds1  12813  pcfac  13073  mgmcl  13622  mhmlin  13722  mhmmulg  13916  issubg2m  13942  nsgbi  13957  srgmulgass  14232  dvdsrtr  14346  issubrng2  14456  issubrg2  14487  domnmuln0  14520  inopn  14994  basis1  15038  cnmpt2t  15284  cnmpt22  15285  cnmptcom  15289  xmeteq0  15350  sincosq1sgn  15817  sincosq2sgn  15818  sincosq3sgn  15819  sincosq4sgn  15820  speano5  16840