Theorem 3impia 1203

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

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

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 983

This theorem is referenced by:  mopick2  2139  3gencl  2811  mob2  2960  moi  2963  reupick3  3466  disjne  3522  elpr2elpr  3830  disji2  4051  tz7.2  4419  funopg  5324  fvun1  5668  fvopab6  5699  isores3  5907  ovmpt4g  6091  ovmpos  6092  ov2gf  6093  ofrval  6192  poxp  6341  smoel  6409  tfr1onlemaccex  6457  tfrcllemaccex  6470  nnaass  6594  qsel  6722  xpdom3m  6954  phpm  6988  ctssdc  7241  mkvprop  7286  prarloclem3  7645  aptisr  7927  axpre-apti  8033  axapti  8178  addn0nid  8481  divvalap  8782  letrp1  8956  p1le  8957  zextle  9499  zextlt  9500  btwnnz  9502  gtndiv  9503  uzind2  9520  fzind  9523  iccleub  10088  uzsubsubfz  10204  elfz0fzfz0  10283  difelfznle  10292  elfzo0le  10346  fzonmapblen  10348  fzofzim  10349  fzosplitprm1  10400  rebtwn2zlemstep  10432  qbtwnxr  10437  icogelb  10445  expcl2lemap  10733  expclzaplem  10745  expnegzap  10755  leexp2r  10775  expnbnd  10845  bcval4  10934  bccmpl  10936  elovmpowrd  11072  ccatval2  11092  wrdl1s1  11122  swrdsb0eq  11156  swrdccatin1  11216  pfxccatpfx2  11228  absexpzap  11506  divalgb  12351  ndvdssub  12356  dvdsgcd  12448  dfgcd2  12450  rplpwr  12463  nnmindc  12470  lcmgcdlem  12514  coprmdvds1  12528  qredeq  12533  prmdvdsexpr  12587  nnnn0modprm0  12693  pcexp  12747  difsqpwdvds  12776  prmpwdvds  12793  elrestr  13194  isnmgm  13307  grpasscan1  13510  grpinvnz  13518  mulgneg2  13607  dvdsrmul1  13979  dvdsunit  13989  lmodlema  14169  mopni  15069  sincosq1lem  15412  rpcxpmul2  15500  logbgcd1irr  15554  gausslemma2dlem1a  15650  gausslemma2dlem2  15654  gausslemma2dlem4  15656  2lgsoddprmlem3  15703  uhgredgrnv  15844