Theorem 3impia 1100

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Hypothesis

Ref	Expression
3impia.1	|- ((ph /\ ps) -> (ch -> th))

Assertion

Ref	Expression
3impia	|- ((ph /\ ps /\ ch) -> th)

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 |- ((ph /\ ps) -> (ch -> th))
2	1	ex 108	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	3imp 1097	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 4   /\ wa 97   /\ w3a 884

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 886

This theorem is referenced by:  mopick2  1980  3gencl  2582  mob2  2715  moi  2718  reupick3  3216  disjne  3267  funopg  4877  fvun1  5182  fvopab6  5207  isores3  5398  ovmpt4g  5565  ovmpt2s  5566  ov2gf  5567  ofrval  5664  poxp  5794  smoel  5856  nnaass  6003  qsel  6119  xpdom3m  6244  prarloclem3  6480  aptisr  6705  axpre-apti  6769  axapti  6887  divvalap  7435  letrp1  7595  p1le  7596  zextle  8107  zextlt  8108  btwnnz  8110  gtndiv  8111  uzind2  8126  fzind  8129  iccleub  8570  uzsubsubfz  8681  elfz0fzfz0  8753  difelfznle  8763  elfzo0le  8811  fzonmapblen  8813  fzofzim  8814  fzosplitprm1  8860  expcl2lemap  8921  expclzaplem  8933  expnegzap  8943  leexp2r  8962  expnbnd  9025