Theorem 3impia 1224

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

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

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 1004

This theorem is referenced by:  mopick2  2161  3gencl  2834  mob2  2983  moi  2986  reupick3  3489  disjne  3545  elpr2elpr  3854  disji2  4075  tz7.2  4445  funopg  5352  fvun1  5702  fvopab6  5733  isores3  5945  ovmpt4g  6133  ovmpos  6134  ov2gf  6135  ofrval  6235  poxp  6384  smoel  6452  tfr1onlemaccex  6500  tfrcllemaccex  6513  nnaass  6639  qsel  6767  xpdom3m  7001  phpm  7035  ctssdc  7291  mkvprop  7336  prarloclem3  7695  aptisr  7977  axpre-apti  8083  axapti  8228  addn0nid  8531  divvalap  8832  letrp1  9006  p1le  9007  zextle  9549  zextlt  9550  btwnnz  9552  gtndiv  9553  uzind2  9570  fzind  9573  iccleub  10139  uzsubsubfz  10255  elfz0fzfz0  10334  difelfznle  10343  elfzo0le  10397  fzonmapblen  10399  fzofzim  10400  fzosplitprm1  10452  rebtwn2zlemstep  10484  qbtwnxr  10489  icogelb  10497  expcl2lemap  10785  expclzaplem  10797  expnegzap  10807  leexp2r  10827  expnbnd  10897  bcval4  10986  bccmpl  10988  elovmpowrd  11126  ccatval2  11146  ccatrcl1  11162  wrdl1s1  11178  swrdsb0eq  11213  swrdccatin1  11273  pfxccatpfx2  11285  absexpzap  11607  divalgb  12452  ndvdssub  12457  dvdsgcd  12549  dfgcd2  12551  rplpwr  12564  nnmindc  12571  lcmgcdlem  12615  coprmdvds1  12629  qredeq  12634  prmdvdsexpr  12688  nnnn0modprm0  12794  pcexp  12848  difsqpwdvds  12877  prmpwdvds  12894  elrestr  13296  isnmgm  13409  grpasscan1  13612  grpinvnz  13620  mulgneg2  13709  dvdsrmul1  14082  dvdsunit  14092  lmodlema  14272  mopni  15172  sincosq1lem  15515  rpcxpmul2  15603  logbgcd1irr  15657  gausslemma2dlem1a  15753  gausslemma2dlem2  15757  gausslemma2dlem4  15759  2lgsoddprmlem3  15806  uhgredgrnv  15952  usgredg4  16029  uspgr2wlkeqi  16113