Theorem 3impib 1201

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

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

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 980

This theorem is referenced by:  mob  2919  eqreu  2929  iotam  5208  funimaexglem  5299  ssimaexg  5578  rbropap  6243  dfsmo2  6287  3ecoptocl  6623  distrnq0  7457  addassnq0  7460  uzind  9362  fzind  9366  fnn0ind  9367  xltnegi  9833  facwordi  10715  shftvalg  10840  shftval4g  10841  mulgcd  12011  coprmdvds1  12085  pcfac  12342  mgmcl  12772  mhmlin  12852  mhmmulg  13017  issubg2m  13042  nsgbi  13057  srgmulgass  13165  dvdsrtr  13263  issubrg2  13362  inopn  13434  basis1  13478  cnmpt2t  13724  cnmpt22  13725  cnmptcom  13729  xmeteq0  13790  sincosq1sgn  14178  sincosq2sgn  14179  sincosq3sgn  14180  sincosq4sgn  14181  speano5  14616