Theorem 3impia 1202

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

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

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 982

This theorem is referenced by:  mopick2  2125  3gencl  2794  mob2  2941  moi  2944  reupick3  3445  disjne  3501  disji2  4023  tz7.2  4386  funopg  5289  fvun1  5624  fvopab6  5655  isores3  5859  ovmpt4g  6042  ovmpos  6043  ov2gf  6044  ofrval  6143  poxp  6287  smoel  6355  tfr1onlemaccex  6403  tfrcllemaccex  6416  nnaass  6540  qsel  6668  xpdom3m  6890  phpm  6923  ctssdc  7174  mkvprop  7219  prarloclem3  7559  aptisr  7841  axpre-apti  7947  axapti  8092  addn0nid  8395  divvalap  8695  letrp1  8869  p1le  8870  zextle  9411  zextlt  9412  btwnnz  9414  gtndiv  9415  uzind2  9432  fzind  9435  iccleub  10000  uzsubsubfz  10116  elfz0fzfz0  10195  difelfznle  10204  elfzo0le  10255  fzonmapblen  10257  fzofzim  10258  fzosplitprm1  10304  rebtwn2zlemstep  10324  qbtwnxr  10329  icogelb  10337  expcl2lemap  10625  expclzaplem  10637  expnegzap  10647  leexp2r  10667  expnbnd  10737  bcval4  10826  bccmpl  10828  elovmpowrd  10958  absexpzap  11227  divalgb  12069  ndvdssub  12074  dvdsgcd  12152  dfgcd2  12154  rplpwr  12167  nnmindc  12174  lcmgcdlem  12218  coprmdvds1  12232  qredeq  12237  prmdvdsexpr  12291  nnnn0modprm0  12396  pcexp  12450  difsqpwdvds  12479  prmpwdvds  12496  elrestr  12861  isnmgm  12946  grpasscan1  13138  grpinvnz  13146  mulgneg2  13229  dvdsrmul1  13601  dvdsunit  13611  lmodlema  13791  mopni  14661  sincosq1lem  15001  logbgcd1irr  15140  gausslemma2dlem1a  15215  gausslemma2dlem2  15219  gausslemma2dlem4  15221  2lgsoddprmlem3  15268