Theorem 3impib 1232

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mob  3008  eqreu  3018  iotam  5369  funimaexglem  5464  ssimaexg  5765  funopdmsn  5895  rbropap  6514  dfsmo2  6558  3ecoptocl  6898  distrnq0  7827  addassnq0  7830  uzind  9762  fzind  9766  fnn0ind  9767  xltnegi  10248  facwordi  11194  shftvalg  11617  shftval4g  11618  mulgcd  12812  coprmdvds1  12888  pcfac  13152  mgmcl  13732  mhmlin  13827  mhmmulg  14019  issubg2m  14045  nsgbi  14060  srgmulgass  14377  dvdsrtr  14492  issubrng2  14602  issubrg2  14633  domnmuln0  14666  inopn  15195  basis1  15239  cnmpt2t  15485  cnmpt22  15486  cnmptcom  15490  xmeteq0  15551  sincosq1sgn  16019  sincosq2sgn  16020  sincosq3sgn  16021  sincosq4sgn  16022  speano5  17136