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  5700  fvopab6  5731  isores3  5939  ovmpt4g  6127  ovmpos  6128  ov2gf  6129  ofrval  6229  poxp  6378  smoel  6446  tfr1onlemaccex  6494  tfrcllemaccex  6507  nnaass  6631  qsel  6759  xpdom3m  6993  phpm  7027  ctssdc  7280  mkvprop  7325  prarloclem3  7684  aptisr  7966  axpre-apti  8072  axapti  8217  addn0nid  8520  divvalap  8821  letrp1  8995  p1le  8996  zextle  9538  zextlt  9539  btwnnz  9541  gtndiv  9542  uzind2  9559  fzind  9562  iccleub  10127  uzsubsubfz  10243  elfz0fzfz0  10322  difelfznle  10331  elfzo0le  10385  fzonmapblen  10387  fzofzim  10388  fzosplitprm1  10440  rebtwn2zlemstep  10472  qbtwnxr  10477  icogelb  10485  expcl2lemap  10773  expclzaplem  10785  expnegzap  10795  leexp2r  10815  expnbnd  10885  bcval4  10974  bccmpl  10976  elovmpowrd  11113  ccatval2  11133  wrdl1s1  11163  swrdsb0eq  11197  swrdccatin1  11257  pfxccatpfx2  11269  absexpzap  11591  divalgb  12436  ndvdssub  12441  dvdsgcd  12533  dfgcd2  12535  rplpwr  12548  nnmindc  12555  lcmgcdlem  12599  coprmdvds1  12613  qredeq  12618  prmdvdsexpr  12672  nnnn0modprm0  12778  pcexp  12832  difsqpwdvds  12861  prmpwdvds  12878  elrestr  13280  isnmgm  13393  grpasscan1  13596  grpinvnz  13604  mulgneg2  13693  dvdsrmul1  14066  dvdsunit  14076  lmodlema  14256  mopni  15156  sincosq1lem  15499  rpcxpmul2  15587  logbgcd1irr  15641  gausslemma2dlem1a  15737  gausslemma2dlem2  15741  gausslemma2dlem4  15743  2lgsoddprmlem3  15790  uhgredgrnv  15936  usgredg4  16013  uspgr2wlkeqi  16078