Theorem 3impia 1202

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

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

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 982

This theorem is referenced by:  mopick2  2125  3gencl  2794  mob2  2940  moi  2943  reupick3  3444  disjne  3500  disji2  4022  tz7.2  4385  funopg  5288  fvun1  5623  fvopab6  5654  isores3  5858  ovmpt4g  6041  ovmpos  6042  ov2gf  6043  ofrval  6141  poxp  6285  smoel  6353  tfr1onlemaccex  6401  tfrcllemaccex  6414  nnaass  6538  qsel  6666  xpdom3m  6888  phpm  6921  ctssdc  7172  mkvprop  7217  prarloclem3  7557  aptisr  7839  axpre-apti  7945  axapti  8090  addn0nid  8393  divvalap  8693  letrp1  8867  p1le  8868  zextle  9408  zextlt  9409  btwnnz  9411  gtndiv  9412  uzind2  9429  fzind  9432  iccleub  9997  uzsubsubfz  10113  elfz0fzfz0  10192  difelfznle  10201  elfzo0le  10252  fzonmapblen  10254  fzofzim  10255  fzosplitprm1  10301  rebtwn2zlemstep  10321  qbtwnxr  10326  icogelb  10334  expcl2lemap  10622  expclzaplem  10634  expnegzap  10644  leexp2r  10664  expnbnd  10734  bcval4  10823  bccmpl  10825  elovmpowrd  10955  absexpzap  11224  divalgb  12066  ndvdssub  12071  dvdsgcd  12149  dfgcd2  12151  rplpwr  12164  nnmindc  12171  lcmgcdlem  12215  coprmdvds1  12229  qredeq  12234  prmdvdsexpr  12288  nnnn0modprm0  12393  pcexp  12447  difsqpwdvds  12476  prmpwdvds  12493  elrestr  12858  isnmgm  12943  grpasscan1  13135  grpinvnz  13143  mulgneg2  13226  dvdsrmul1  13598  dvdsunit  13608  lmodlema  13788  mopni  14650  sincosq1lem  14960  logbgcd1irr  15099  gausslemma2dlem1a  15174  gausslemma2dlem2  15178  gausslemma2dlem4  15180  2lgsoddprmlem3  15199