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  5369  funimaexglem  5464  ssimaexg  5765  funopdmsn  5895  rbropap  6514  dfsmo2  6558  3ecoptocl  6898  distrnq0  7826  addassnq0  7829  uzind  9761  fzind  9765  fnn0ind  9766  xltnegi  10247  facwordi  11192  shftvalg  11615  shftval4g  11616  mulgcd  12809  coprmdvds1  12885  pcfac  13149  mgmcl  13728  mhmlin  13823  mhmmulg  14015  issubg2m  14041  nsgbi  14056  srgmulgass  14342  dvdsrtr  14457  issubrng2  14567  issubrg2  14598  domnmuln0  14631  inopn  15153  basis1  15197  cnmpt2t  15443  cnmpt22  15444  cnmptcom  15448  xmeteq0  15509  sincosq1sgn  15977  sincosq2sgn  15978  sincosq3sgn  15979  sincosq4sgn  15980  speano5  17068