Theorem 3impib 1225

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

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

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 1004

This theorem is referenced by:  mob  2985  eqreu  2995  iotam  5310  funimaexglem  5404  ssimaexg  5698  funopdmsn  5823  rbropap  6395  dfsmo2  6439  3ecoptocl  6779  distrnq0  7657  addassnq0  7660  uzind  9569  fzind  9573  fnn0ind  9574  xltnegi  10043  facwordi  10974  shftvalg  11362  shftval4g  11363  mulgcd  12552  coprmdvds1  12628  pcfac  12888  mgmcl  13407  mhmlin  13515  mhmmulg  13715  issubg2m  13741  nsgbi  13756  srgmulgass  13967  dvdsrtr  14080  issubrng2  14189  issubrg2  14220  domnmuln0  14252  inopn  14692  basis1  14736  cnmpt2t  14982  cnmpt22  14983  cnmptcom  14987  xmeteq0  15048  sincosq1sgn  15515  sincosq2sgn  15516  sincosq3sgn  15517  sincosq4sgn  15518  speano5  16362