Theorem 3impia 1231

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mopick2  2170  3gencl  2856  mob2  3006  moi  3009  reupick3  3518  disjne  3578  elpr2elpr  3901  disji2  4122  tz7.2  4499  funopg  5411  fvun1  5769  fvopab6  5805  isores3  6021  ovmpt4g  6211  ovmpos  6212  ov2gf  6213  ofrval  6313  poxp  6468  smoel  6571  tfr1onlemaccex  6619  tfrcllemaccex  6632  nnaass  6758  qsel  6886  xpdom3m  7132  phpm  7167  ctssdc  7453  mkvprop  7498  prarloclem3  7864  aptisr  8146  axpre-apti  8252  axapti  8396  addn0nid  8701  divvalap  9006  letrp1  9180  p1le  9181  zextle  9741  zextlt  9742  btwnnz  9744  gtndiv  9745  uzind2  9762  fzind  9765  iccleub  10343  uzsubsubfz  10462  elfz0fzfz0  10543  difelfznle  10552  elfzo0le  10607  fzonmapblen  10609  fzofzim  10610  fzosplitprm1  10663  rebtwn2zlemstep  10697  qbtwnxr  10702  icogelb  10710  expcl2lemap  11001  expclzaplem  11013  expnegzap  11023  leexp2r  11043  expnbnd  11114  bcval4  11204  bccmpl  11206  bcm1n  11221  elovmpowrd  11360  ccatval2  11380  ccatrcl1  11396  wrdl1s1  11412  ccat2s1fvwd  11429  swrdsb0eq  11451  swrdccatin1  11511  pfxccatpfx2  11523  absexpzap  11861  divalgb  12708  ndvdssub  12713  dvdsgcd  12805  dfgcd2  12807  rplpwr  12820  nnmindc  12827  lcmgcdlem  12871  coprmdvds1  12885  qredeq  12890  prmdvdsexpr  12945  nnnn0modprm0  13054  pcexp  13108  difsqpwdvds  13137  prmpwdvds  13154  elrestr  13650  isnmgm  13729  grpasscan1  13917  grpinvnz  13925  mulgneg2  14008  dvdsrmul1  14458  dvdsunit  14468  lmodlema  14677  mopni  15632  sincosq1lem  15976  rpcxpmul2  16068  logbgcd1irr  16122  bcmono  16202  gausslemma2dlem1a  16275  gausslemma2dlem2  16279  gausslemma2dlem4  16281  2lgsoddprmlem3  16328  uhgredgrnv  16477  usgredg4  16554  usgr2v1e2w  16585  uspgr2wlkeqi  16706  eupth2lem3lem4fi  16812