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  2989  eqreu  2999  iotam  5325  funimaexglem  5420  ssimaexg  5717  funopdmsn  5842  rbropap  6452  dfsmo2  6496  3ecoptocl  6836  distrnq0  7722  addassnq0  7725  uzind  9635  fzind  9639  fnn0ind  9640  xltnegi  10114  facwordi  11048  shftvalg  11459  shftval4g  11460  mulgcd  12650  coprmdvds1  12726  pcfac  12986  mgmcl  13505  mhmlin  13613  mhmmulg  13813  issubg2m  13839  nsgbi  13854  srgmulgass  14066  dvdsrtr  14179  issubrng2  14288  issubrg2  14319  domnmuln0  14352  inopn  14797  basis1  14841  cnmpt2t  15087  cnmpt22  15088  cnmptcom  15092  xmeteq0  15153  sincosq1sgn  15620  sincosq2sgn  15621  sincosq3sgn  15622  sincosq4sgn  15623  speano5  16643