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 )

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

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 1011

This theorem is referenced by:  mopick2  2170  3gencl  2856  mob2  3006  moi  3009  reupick3  3518  disjne  3577  elpr2elpr  3896  disji2  4117  tz7.2  4494  funopg  5406  fvun1  5763  fvopab6  5796  isores3  6011  ovmpt4g  6201  ovmpos  6202  ov2gf  6203  ofrval  6303  poxp  6458  smoel  6561  tfr1onlemaccex  6609  tfrcllemaccex  6622  nnaass  6748  qsel  6876  xpdom3m  7122  phpm  7157  ctssdc  7443  mkvprop  7488  prarloclem3  7854  aptisr  8136  axpre-apti  8242  axapti  8386  addn0nid  8690  divvalap  8994  letrp1  9168  p1le  9169  zextle  9716  zextlt  9717  btwnnz  9719  gtndiv  9720  uzind2  9737  fzind  9740  iccleub  10312  uzsubsubfz  10430  elfz0fzfz0  10511  difelfznle  10520  elfzo0le  10575  fzonmapblen  10577  fzofzim  10578  fzosplitprm1  10631  rebtwn2zlemstep  10665  qbtwnxr  10670  icogelb  10678  expcl2lemap  10966  expclzaplem  10978  expnegzap  10988  leexp2r  11008  expnbnd  11079  bcval4  11168  bccmpl  11170  bcm1n  11185  elovmpowrd  11324  ccatval2  11344  ccatrcl1  11360  wrdl1s1  11376  ccat2s1fvwd  11393  swrdsb0eq  11415  swrdccatin1  11475  pfxccatpfx2  11487  absexpzap  11824  divalgb  12670  ndvdssub  12675  dvdsgcd  12767  dfgcd2  12769  rplpwr  12782  nnmindc  12789  lcmgcdlem  12833  coprmdvds1  12847  qredeq  12852  prmdvdsexpr  12906  nnnn0modprm0  13012  pcexp  13066  difsqpwdvds  13095  prmpwdvds  13112  elrestr  13578  isnmgm  13657  grpasscan1  13845  grpinvnz  13853  mulgneg2  13936  dvdsrmul1  14382  dvdsunit  14392  lmodlema  14601  mopni  15506  sincosq1lem  15849  rpcxpmul2  15938  logbgcd1irr  15992  gausslemma2dlem1a  16091  gausslemma2dlem2  16095  gausslemma2dlem4  16097  2lgsoddprmlem3  16144  uhgredgrnv  16293  usgredg4  16370  usgr2v1e2w  16401  uspgr2wlkeqi  16522  eupth2lem3lem4fi  16628