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  7454  mkvprop  7499  prarloclem3  7865  aptisr  8147  axpre-apti  8253  axapti  8397  addn0nid  8702  divvalap  9007  letrp1  9181  p1le  9182  zextle  9742  zextlt  9743  btwnnz  9745  gtndiv  9746  uzind2  9763  fzind  9766  iccleub  10344  uzsubsubfz  10463  elfz0fzfz0  10544  difelfznle  10553  elfzo0le  10608  fzonmapblen  10610  fzofzim  10611  fzosplitprm1  10664  rebtwn2zlemstep  10698  qbtwnxr  10703  icogelb  10711  expcl2lemap  11003  expclzaplem  11015  expnegzap  11025  leexp2r  11045  expnbnd  11116  bcval4  11206  bccmpl  11208  bcm1n  11223  elovmpowrd  11362  ccatval2  11382  ccatrcl1  11398  wrdl1s1  11414  ccat2s1fvwd  11431  swrdsb0eq  11453  swrdccatin1  11513  pfxccatpfx2  11525  absexpzap  11863  divalgb  12711  ndvdssub  12716  dvdsgcd  12808  dfgcd2  12810  rplpwr  12823  nnmindc  12830  lcmgcdlem  12874  coprmdvds1  12888  qredeq  12893  prmdvdsexpr  12948  nnnn0modprm0  13057  pcexp  13111  difsqpwdvds  13140  prmpwdvds  13157  elrestr  13654  isnmgm  13733  grpasscan1  13921  grpinvnz  13929  mulgneg2  14012  dvdsrmul1  14493  dvdsunit  14503  lmodlema  14712  mopni  15674  sincosq1lem  16018  rpcxpmul2  16110  logbgcd1irr  16164  bcmono  16265  gausslemma2dlem1a  16343  gausslemma2dlem2  16347  gausslemma2dlem4  16349  2lgsoddprmlem3  16396  uhgredgrnv  16545  usgredg4  16622  usgr2v1e2w  16653  uspgr2wlkeqi  16774  eupth2lem3lem4fi  16880