Theorem 3impia 1101

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

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

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 887

This theorem is referenced by:  mopick2  1983  3gencl  2588  mob2  2721  moi  2724  reupick3  3222  disjne  3273  tz7.2  4091  funopg  4934  fvun1  5239  fvopab6  5264  isores3  5455  ovmpt4g  5623  ovmpt2s  5624  ov2gf  5625  ofrval  5722  poxp  5853  smoel  5915  nnaass  6064  qsel  6183  xpdom3m  6308  phpm  6327  prarloclem3  6595  aptisr  6863  axpre-apti  6959  axapti  7090  divvalap  7653  letrp1  7814  p1le  7815  zextle  8331  zextlt  8332  btwnnz  8334  gtndiv  8335  uzind2  8350  fzind  8353  iccleub  8800  uzsubsubfz  8911  elfz0fzfz0  8983  difelfznle  8993  elfzo0le  9041  fzonmapblen  9043  fzofzim  9044  fzosplitprm1  9090  qbtwnzlemstep  9103  rebtwn2zlemstep  9107  expcl2lemap  9267  expclzaplem  9279  expnegzap  9289  leexp2r  9308  expnbnd  9372  absexpzap  9676