Theorem 3impib 1204

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

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

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 983

This theorem is referenced by:  mob  2955  eqreu  2965  iotam  5263  funimaexglem  5357  ssimaexg  5641  funopdmsn  5764  rbropap  6329  dfsmo2  6373  3ecoptocl  6711  distrnq0  7572  addassnq0  7575  uzind  9484  fzind  9488  fnn0ind  9489  xltnegi  9957  facwordi  10885  shftvalg  11147  shftval4g  11148  mulgcd  12337  coprmdvds1  12413  pcfac  12673  mgmcl  13191  mhmlin  13299  mhmmulg  13499  issubg2m  13525  nsgbi  13540  srgmulgass  13751  dvdsrtr  13863  issubrng2  13972  issubrg2  14003  domnmuln0  14035  inopn  14475  basis1  14519  cnmpt2t  14765  cnmpt22  14766  cnmptcom  14770  xmeteq0  14831  sincosq1sgn  15298  sincosq2sgn  15299  sincosq3sgn  15300  sincosq4sgn  15301  speano5  15880