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  2986  eqreu  2996  iotam  5316  funimaexglem  5410  ssimaexg  5704  funopdmsn  5829  rbropap  6404  dfsmo2  6448  3ecoptocl  6788  distrnq0  7669  addassnq0  7672  uzind  9581  fzind  9585  fnn0ind  9586  xltnegi  10060  facwordi  10992  shftvalg  11387  shftval4g  11388  mulgcd  12577  coprmdvds1  12653  pcfac  12913  mgmcl  13432  mhmlin  13540  mhmmulg  13740  issubg2m  13766  nsgbi  13781  srgmulgass  13992  dvdsrtr  14105  issubrng2  14214  issubrg2  14245  domnmuln0  14277  inopn  14717  basis1  14761  cnmpt2t  15007  cnmpt22  15008  cnmptcom  15012  xmeteq0  15073  sincosq1sgn  15540  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  speano5  16475