Theorem 3impib 1227

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

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

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 1006

This theorem is referenced by:  mob  2988  eqreu  2998  iotam  5318  funimaexglem  5413  ssimaexg  5708  funopdmsn  5833  rbropap  6408  dfsmo2  6452  3ecoptocl  6792  distrnq0  7678  addassnq0  7681  uzind  9590  fzind  9594  fnn0ind  9595  xltnegi  10069  facwordi  11001  shftvalg  11396  shftval4g  11397  mulgcd  12586  coprmdvds1  12662  pcfac  12922  mgmcl  13441  mhmlin  13549  mhmmulg  13749  issubg2m  13775  nsgbi  13790  srgmulgass  14001  dvdsrtr  14114  issubrng2  14223  issubrg2  14254  domnmuln0  14286  inopn  14726  basis1  14770  cnmpt2t  15016  cnmpt22  15017  cnmptcom  15021  xmeteq0  15082  sincosq1sgn  15549  sincosq2sgn  15550  sincosq3sgn  15551  sincosq4sgn  15552  speano5  16539