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  7826  addassnq0  7829  uzind  9757  fzind  9761  fnn0ind  9762  xltnegi  10237  facwordi  11178  shftvalg  11601  shftval4g  11602  mulgcd  12793  coprmdvds1  12869  pcfac  13129  mgmcl  13679  mhmlin  13774  mhmmulg  13966  issubg2m  13992  nsgbi  14007  srgmulgass  14293  dvdsrtr  14408  issubrng2  14518  issubrg2  14549  domnmuln0  14582  inopn  15104  basis1  15148  cnmpt2t  15394  cnmpt22  15395  cnmptcom  15399  xmeteq0  15460  sincosq1sgn  15927  sincosq2sgn  15928  sincosq3sgn  15929  sincosq4sgn  15930  speano5  16970