Theorem 3impia 1227

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

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

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 1007

This theorem is referenced by:  mopick2  2164  3gencl  2848  mob2  2997  moi  3000  reupick3  3506  disjne  3562  elpr2elpr  3880  disji2  4101  tz7.2  4475  funopg  5386  fvun1  5743  fvopab6  5774  isores3  5988  ovmpt4g  6176  ovmpos  6177  ov2gf  6178  ofrval  6277  poxp  6428  smoel  6531  tfr1onlemaccex  6579  tfrcllemaccex  6592  nnaass  6718  qsel  6846  xpdom3m  7085  phpm  7120  ctssdc  7404  mkvprop  7449  prarloclem3  7812  aptisr  8094  axpre-apti  8200  axapti  8344  addn0nid  8647  divvalap  8948  letrp1  9122  p1le  9123  zextle  9669  zextlt  9670  btwnnz  9672  gtndiv  9673  uzind2  9690  fzind  9693  iccleub  10264  uzsubsubfz  10381  elfz0fzfz0  10460  difelfznle  10469  elfzo0le  10524  fzonmapblen  10526  fzofzim  10527  fzosplitprm1  10580  rebtwn2zlemstep  10612  qbtwnxr  10617  icogelb  10625  expcl2lemap  10913  expclzaplem  10925  expnegzap  10935  leexp2r  10955  expnbnd  11025  bcval4  11114  bccmpl  11116  bcm1n  11131  elovmpowrd  11266  ccatval2  11286  ccatrcl1  11302  wrdl1s1  11318  ccat2s1fvwd  11335  swrdsb0eq  11357  swrdccatin1  11417  pfxccatpfx2  11429  absexpzap  11765  divalgb  12611  ndvdssub  12616  dvdsgcd  12708  dfgcd2  12710  rplpwr  12723  nnmindc  12730  lcmgcdlem  12774  coprmdvds1  12788  qredeq  12793  prmdvdsexpr  12847  nnnn0modprm0  12953  pcexp  13007  difsqpwdvds  13036  prmpwdvds  13053  elrestr  13460  isnmgm  13573  grpasscan1  13776  grpinvnz  13784  mulgneg2  13873  dvdsrmul1  14247  dvdsunit  14257  lmodlema  14440  mopni  15347  sincosq1lem  15690  rpcxpmul2  15778  logbgcd1irr  15832  gausslemma2dlem1a  15931  gausslemma2dlem2  15935  gausslemma2dlem4  15937  2lgsoddprmlem3  15984  uhgredgrnv  16133  usgredg4  16210  usgr2v1e2w  16241  uspgr2wlkeqi  16362  eupth2lem3lem4fi  16468