Theorem 3impib 1228

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

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

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 1007

This theorem is referenced by:  mob  2999  eqreu  3009  iotam  5344  funimaexglem  5439  ssimaexg  5739  funopdmsn  5864  rbropap  6474  dfsmo2  6518  3ecoptocl  6858  distrnq0  7774  addassnq0  7777  uzind  9689  fzind  9693  fnn0ind  9694  xltnegi  10168  facwordi  11102  shftvalg  11521  shftval4g  11522  mulgcd  12712  coprmdvds1  12788  pcfac  13048  mgmcl  13572  mhmlin  13680  mhmmulg  13880  issubg2m  13906  nsgbi  13921  srgmulgass  14133  dvdsrtr  14246  issubrng2  14355  issubrg2  14386  domnmuln0  14419  inopn  14868  basis1  14912  cnmpt2t  15158  cnmpt22  15159  cnmptcom  15163  xmeteq0  15224  sincosq1sgn  15691  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  speano5  16714