Theorem 3impia 1178

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 114	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1175	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  mopick2  2080  3gencl  2715  mob2  2859  moi  2862  reupick3  3356  disjne  3411  disji2  3917  tz7.2  4271  funopg  5152  fvun1  5480  fvopab6  5510  isores3  5709  ovmpt4g  5886  ovmpos  5887  ov2gf  5888  ofrval  5985  poxp  6122  smoel  6190  tfr1onlemaccex  6238  tfrcllemaccex  6251  nnaass  6374  qsel  6499  xpdom3m  6721  phpm  6752  ctssdc  6991  mkvprop  7025  prarloclem3  7298  aptisr  7580  axpre-apti  7686  axapti  7828  addn0nid  8129  divvalap  8427  letrp1  8599  p1le  8600  zextle  9135  zextlt  9136  btwnnz  9138  gtndiv  9139  uzind2  9156  fzind  9159  iccleub  9707  uzsubsubfz  9820  elfz0fzfz0  9896  difelfznle  9905  elfzo0le  9955  fzonmapblen  9957  fzofzim  9958  fzosplitprm1  10004  rebtwn2zlemstep  10023  qbtwnxr  10028  expcl2lemap  10298  expclzaplem  10310  expnegzap  10320  leexp2r  10340  expnbnd  10408  bcval4  10491  bccmpl  10493  absexpzap  10845  divalgb  11611  ndvdssub  11616  dvdsgcd  11689  dfgcd2  11691  rplpwr  11704  lcmgcdlem  11747  coprmdvds1  11761  qredeq  11766  prmdvdsexpr  11817  elrestr  12117  mopni  12640  sincosq1lem  12895