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  14384  dvdsrtr  14499  issubrng2  14609  issubrg2  14640  domnmuln0  14673  inopn  15203  basis1  15247  cnmpt2t  15493  cnmpt22  15494  cnmptcom  15498  xmeteq0  15559  sincosq1sgn  16027  sincosq2sgn  16028  sincosq3sgn  16029  sincosq4sgn  16030  speano5  17149