Theorem 3impib 1201

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

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

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 980

This theorem is referenced by:  mob  2921  eqreu  2931  iotam  5210  funimaexglem  5301  ssimaexg  5580  rbropap  6246  dfsmo2  6290  3ecoptocl  6626  distrnq0  7460  addassnq0  7463  uzind  9366  fzind  9370  fnn0ind  9371  xltnegi  9837  facwordi  10722  shftvalg  10847  shftval4g  10848  mulgcd  12019  coprmdvds1  12093  pcfac  12350  mgmcl  12783  mhmlin  12863  mhmmulg  13029  issubg2m  13054  nsgbi  13069  srgmulgass  13177  dvdsrtr  13275  issubrg2  13367  inopn  13588  basis1  13632  cnmpt2t  13878  cnmpt22  13879  cnmptcom  13883  xmeteq0  13944  sincosq1sgn  14332  sincosq2sgn  14333  sincosq3sgn  14334  sincosq4sgn  14335  speano5  14781