Theorem 3impib 1232

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

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

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 1011

This theorem is referenced by:  mob  3008  eqreu  3018  iotam  5364  funimaexglem  5459  ssimaexg  5759  funopdmsn  5886  rbropap  6504  dfsmo2  6548  3ecoptocl  6888  distrnq0  7816  addassnq0  7819  uzind  9736  fzind  9740  fnn0ind  9741  xltnegi  10216  facwordi  11156  shftvalg  11579  shftval4g  11580  mulgcd  12771  coprmdvds1  12847  pcfac  13107  mgmcl  13656  mhmlin  13751  mhmmulg  13943  issubg2m  13969  nsgbi  13984  srgmulgass  14267  dvdsrtr  14381  issubrng2  14491  issubrg2  14522  domnmuln0  14555  inopn  15027  basis1  15071  cnmpt2t  15317  cnmpt22  15318  cnmptcom  15322  xmeteq0  15383  sincosq1sgn  15850  sincosq2sgn  15851  sincosq3sgn  15852  sincosq4sgn  15853  speano5  16884