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  2163  3gencl  2838  mob2  2987  moi  2990  reupick3  3494  disjne  3550  elpr2elpr  3864  disji2  4085  tz7.2  4457  funopg  5367  fvun1  5721  fvopab6  5752  isores3  5966  ovmpt4g  6154  ovmpos  6155  ov2gf  6156  ofrval  6255  poxp  6406  smoel  6509  tfr1onlemaccex  6557  tfrcllemaccex  6570  nnaass  6696  qsel  6824  xpdom3m  7061  phpm  7095  ctssdc  7372  mkvprop  7417  prarloclem3  7777  aptisr  8059  axpre-apti  8165  axapti  8309  addn0nid  8612  divvalap  8913  letrp1  9087  p1le  9088  zextle  9632  zextlt  9633  btwnnz  9635  gtndiv  9636  uzind2  9653  fzind  9656  iccleub  10227  uzsubsubfz  10344  elfz0fzfz0  10423  difelfznle  10432  elfzo0le  10487  fzonmapblen  10489  fzofzim  10490  fzosplitprm1  10543  rebtwn2zlemstep  10575  qbtwnxr  10580  icogelb  10588  expcl2lemap  10876  expclzaplem  10888  expnegzap  10898  leexp2r  10918  expnbnd  10988  bcval4  11077  bccmpl  11079  elovmpowrd  11221  ccatval2  11241  ccatrcl1  11257  wrdl1s1  11273  ccat2s1fvwd  11290  swrdsb0eq  11312  swrdccatin1  11372  pfxccatpfx2  11384  absexpzap  11720  divalgb  12566  ndvdssub  12571  dvdsgcd  12663  dfgcd2  12665  rplpwr  12678  nnmindc  12685  lcmgcdlem  12729  coprmdvds1  12743  qredeq  12748  prmdvdsexpr  12802  nnnn0modprm0  12908  pcexp  12962  difsqpwdvds  12991  prmpwdvds  13008  elrestr  13410  isnmgm  13523  grpasscan1  13726  grpinvnz  13734  mulgneg2  13823  dvdsrmul1  14197  dvdsunit  14207  lmodlema  14388  mopni  15293  sincosq1lem  15636  rpcxpmul2  15724  logbgcd1irr  15778  gausslemma2dlem1a  15877  gausslemma2dlem2  15881  gausslemma2dlem4  15883  2lgsoddprmlem3  15930  uhgredgrnv  16079  usgredg4  16156  usgr2v1e2w  16187  uspgr2wlkeqi  16308  eupth2lem3lem4fi  16414