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  2954  eqreu  2964  iotam  5262  funimaexglem  5356  ssimaexg  5640  funopdmsn  5763  rbropap  6328  dfsmo2  6372  3ecoptocl  6710  distrnq0  7571  addassnq0  7574  uzind  9483  fzind  9487  fnn0ind  9488  xltnegi  9956  facwordi  10883  shftvalg  11118  shftval4g  11119  mulgcd  12308  coprmdvds1  12384  pcfac  12644  mgmcl  13162  mhmlin  13270  mhmmulg  13470  issubg2m  13496  nsgbi  13511  srgmulgass  13722  dvdsrtr  13834  issubrng2  13943  issubrg2  13974  domnmuln0  14006  inopn  14446  basis1  14490  cnmpt2t  14736  cnmpt22  14737  cnmptcom  14741  xmeteq0  14802  sincosq1sgn  15269  sincosq2sgn  15270  sincosq3sgn  15271  sincosq4sgn  15272  speano5  15842