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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mob  3008  eqreu  3018  iotam  5372  funimaexglem  5467  ssimaexg  5768  funopdmsn  5898  rbropap  6518  dfsmo2  6562  3ecoptocl  6902  distrnq0  7832  addassnq0  7835  uzind  9768  fzind  9772  fnn0ind  9773  xltnegi  10254  facwordi  11200  shftvalg  11623  shftval4g  11624  mulgcd  12818  coprmdvds1  12894  pcfac  13158  mgmcl  13738  mhmlin  13833  mhmmulg  14025  issubg2m  14051  nsgbi  14066  gsumcom2fi  14275  srgmulgass  14400  dvdsrtr  14517  issubrng2  14627  issubrg2  14658  domnmuln0  14691  inopn  15229  basis1  15273  cnmpt2t  15519  cnmpt22  15520  cnmptcom  15524  xmeteq0  15585  sincosq1sgn  16053  sincosq2sgn  16054  sincosq3sgn  16055  sincosq4sgn  16056  speano5  17175