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  2946  eqreu  2956  iotam  5251  funimaexglem  5342  ssimaexg  5626  rbropap  6310  dfsmo2  6354  3ecoptocl  6692  distrnq0  7543  addassnq0  7546  uzind  9454  fzind  9458  fnn0ind  9459  xltnegi  9927  facwordi  10849  shftvalg  11018  shftval4g  11019  mulgcd  12208  coprmdvds1  12284  pcfac  12544  mgmcl  13061  mhmlin  13169  mhmmulg  13369  issubg2m  13395  nsgbi  13410  srgmulgass  13621  dvdsrtr  13733  issubrng2  13842  issubrg2  13873  domnmuln0  13905  inopn  14323  basis1  14367  cnmpt2t  14613  cnmpt22  14614  cnmptcom  14618  xmeteq0  14679  sincosq1sgn  15146  sincosq2sgn  15147  sincosq3sgn  15148  sincosq4sgn  15149  speano5  15674