Theorem 3impia 1159

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

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

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

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

This theorem is referenced by:  mopick2  2056  3gencl  2689  mob2  2831  moi  2834  reupick3  3325  disjne  3380  disji2  3886  tz7.2  4234  funopg  5113  fvun1  5439  fvopab6  5469  isores3  5668  ovmpt4g  5845  ovmpos  5846  ov2gf  5847  ofrval  5944  poxp  6081  smoel  6149  tfr1onlemaccex  6197  tfrcllemaccex  6210  nnaass  6333  qsel  6458  xpdom3m  6679  phpm  6710  ctssdc  6948  mkvprop  6979  prarloclem3  7247  aptisr  7515  axpre-apti  7614  axapti  7753  addn0nid  8049  divvalap  8341  letrp1  8510  p1le  8511  zextle  9040  zextlt  9041  btwnnz  9043  gtndiv  9044  uzind2  9061  fzind  9064  iccleub  9601  uzsubsubfz  9714  elfz0fzfz0  9790  difelfznle  9799  elfzo0le  9849  fzonmapblen  9851  fzofzim  9852  fzosplitprm1  9898  rebtwn2zlemstep  9917  qbtwnxr  9922  expcl2lemap  10192  expclzaplem  10204  expnegzap  10214  leexp2r  10234  expnbnd  10302  bcval4  10385  bccmpl  10387  absexpzap  10738  divalgb  11464  ndvdssub  11469  dvdsgcd  11540  dfgcd2  11542  rplpwr  11555  lcmgcdlem  11598  coprmdvds1  11612  qredeq  11617  prmdvdsexpr  11668  elrestr  11965  mopni  12465