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  6519  dfsmo2  6563  3ecoptocl  6903  distrnq0  7832  addassnq0  7835  uzind  9767  fzind  9771  fnn0ind  9772  xltnegi  10253  facwordi  11199  shftvalg  11622  shftval4g  11623  mulgcd  12817  coprmdvds1  12893  pcfac  13157  mgmcl  13737  mhmlin  13832  mhmmulg  14024  issubg2m  14050  nsgbi  14065  gsumcom2fi  14274  srgmulgass  14399  dvdsrtr  14516  issubrng2  14626  issubrg2  14657  domnmuln0  14690  inopn  15246  basis1  15290  cnmpt2t  15536  cnmpt22  15537  cnmptcom  15541  xmeteq0  15602  sincosq1sgn  16070  sincosq2sgn  16071  sincosq3sgn  16072  sincosq4sgn  16073  speano5  17192