Theorem 3impia 1200

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

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

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 980

This theorem is referenced by:  mopick2  2109  3gencl  2771  mob2  2917  moi  2920  reupick3  3420  disjne  3476  disji2  3996  tz7.2  4354  funopg  5250  fvun1  5582  fvopab6  5612  isores3  5815  ovmpt4g  5996  ovmpos  5997  ov2gf  5998  ofrval  6092  poxp  6232  smoel  6300  tfr1onlemaccex  6348  tfrcllemaccex  6361  nnaass  6485  qsel  6611  xpdom3m  6833  phpm  6864  ctssdc  7111  mkvprop  7155  prarloclem3  7495  aptisr  7777  axpre-apti  7883  axapti  8026  addn0nid  8329  divvalap  8629  letrp1  8803  p1le  8804  zextle  9342  zextlt  9343  btwnnz  9345  gtndiv  9346  uzind2  9363  fzind  9366  iccleub  9929  uzsubsubfz  10044  elfz0fzfz0  10123  difelfznle  10132  elfzo0le  10182  fzonmapblen  10184  fzofzim  10185  fzosplitprm1  10231  rebtwn2zlemstep  10250  qbtwnxr  10255  icogelb  10263  expcl2lemap  10529  expclzaplem  10541  expnegzap  10551  leexp2r  10571  expnbnd  10640  bcval4  10727  bccmpl  10729  absexpzap  11084  divalgb  11924  ndvdssub  11929  dvdsgcd  12007  dfgcd2  12009  rplpwr  12022  nnmindc  12029  lcmgcdlem  12071  coprmdvds1  12085  qredeq  12090  prmdvdsexpr  12144  nnnn0modprm0  12249  pcexp  12303  difsqpwdvds  12331  prmpwdvds  12347  elrestr  12690  isnmgm  12773  grpasscan1  12927  grpinvnz  12935  mulgneg2  13010  dvdsrmul1  13264  dvdsunit  13274  mopni  13913  sincosq1lem  14177  logbgcd1irr  14316