Theorem 3impib 1204

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

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

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 983

This theorem is referenced by:  mob  2962  eqreu  2972  iotam  5282  funimaexglem  5376  ssimaexg  5664  funopdmsn  5787  rbropap  6352  dfsmo2  6396  3ecoptocl  6734  distrnq0  7607  addassnq0  7610  uzind  9519  fzind  9523  fnn0ind  9524  xltnegi  9992  facwordi  10922  shftvalg  11262  shftval4g  11263  mulgcd  12452  coprmdvds1  12528  pcfac  12788  mgmcl  13306  mhmlin  13414  mhmmulg  13614  issubg2m  13640  nsgbi  13655  srgmulgass  13866  dvdsrtr  13978  issubrng2  14087  issubrg2  14118  domnmuln0  14150  inopn  14590  basis1  14634  cnmpt2t  14880  cnmpt22  14881  cnmptcom  14885  xmeteq0  14946  sincosq1sgn  15413  sincosq2sgn  15414  sincosq3sgn  15415  sincosq4sgn  15416  speano5  16079