Theorem 3impib 1203

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

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

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 982

This theorem is referenced by:  mob  2942  eqreu  2952  iotam  5246  funimaexglem  5337  ssimaexg  5619  rbropap  6296  dfsmo2  6340  3ecoptocl  6678  distrnq0  7519  addassnq0  7522  uzind  9428  fzind  9432  fnn0ind  9433  xltnegi  9901  facwordi  10811  shftvalg  10980  shftval4g  10981  mulgcd  12153  coprmdvds1  12229  pcfac  12488  mgmcl  12942  mhmlin  13039  mhmmulg  13233  issubg2m  13259  nsgbi  13274  srgmulgass  13485  dvdsrtr  13597  issubrng2  13706  issubrg2  13737  domnmuln0  13769  inopn  14171  basis1  14215  cnmpt2t  14461  cnmpt22  14462  cnmptcom  14466  xmeteq0  14527  sincosq1sgn  14961  sincosq2sgn  14962  sincosq3sgn  14963  sincosq4sgn  14964  speano5  15436