Theorem 3impib 1225

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

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

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 1004

This theorem is referenced by:  mob  2985  eqreu  2995  iotam  5309  funimaexglem  5403  ssimaexg  5695  funopdmsn  5818  rbropap  6387  dfsmo2  6431  3ecoptocl  6769  distrnq0  7642  addassnq0  7645  uzind  9554  fzind  9558  fnn0ind  9559  xltnegi  10027  facwordi  10957  shftvalg  11342  shftval4g  11343  mulgcd  12532  coprmdvds1  12608  pcfac  12868  mgmcl  13387  mhmlin  13495  mhmmulg  13695  issubg2m  13721  nsgbi  13736  srgmulgass  13947  dvdsrtr  14059  issubrng2  14168  issubrg2  14199  domnmuln0  14231  inopn  14671  basis1  14715  cnmpt2t  14961  cnmpt22  14962  cnmptcom  14966  xmeteq0  15027  sincosq1sgn  15494  sincosq2sgn  15495  sincosq3sgn  15496  sincosq4sgn  15497  speano5  16265