Theorem 3impia 1261

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 450	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1256	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  mopick2  2540  3gencl  3237  vtoclgft  3254  mob2  3386  moi  3389  reupick3  3912  disjne  4022  elpr2elpr  4398  disji2  4636  disji  4637  tz7.2  5098  sofld  5581  ordintdif  5774  funopg  5922  fvun1  6269  fvopab6  6310  fveqressseq  6355  fvcofneq  6367  fprg  6422  2f1fvneq  6517  isores3  6585  ovmpt4g  6783  ovmpt2s  6784  ov2gf  6785  ofrval  6907  sorpssuni  6946  sorpssint  6947  poxp  7289  suppss2  7329  smoel  7457  smoord  7462  smogt  7464  oaass  7641  oewordi  7671  oeoalem  7676  oeoelem  7678  nnawordi  7701  nnaass  7702  qsel  7826  xpdom3  8058  onsdominel  8109  mapdom3  8132  fisseneq  8171  cantnflem1  8586  cfslbn  9089  cfsmolem  9092  cfcoflem  9094  infpssrlem4  9128  fin23lem7  9138  fin23lem25  9146  isf34lem7  9201  hsmexlem2  9249  axcc3  9260  axdc4lem  9277  tskss  9580  gruss  9618  gruurn  9620  gruiun  9621  gruel  9625  gruen  9634  grudomon  9639  grothac  9652  axpre-sup  9990  axsup  10113  addn0nid  10451  letrp1  10865  p1le  10866  lemul1a  10877  infrelb  11008  zextle  11450  zextlt  11451  btwnnz  11453  gtndiv  11454  uzind2  11470  fzind  11475  eluzsub  11717  zsupss  11777  xrltne  11994  lemaxle  12026  qbtwnre  12030  qbtwnxr  12031  xlemul1a  12118  icogelb  12225  iccleub  12229  iccsplit  12305  uzsubsubfz  12363  elfz0fzfz0  12444  difelfznle  12453  fvffz0  12457  elfzo0le  12511  fzonmapblen  12513  fzofzim  12514  ceile  12648  modadd1  12707  muladdmodid  12710  modmul1  12723  modirr  12741  fsuppmapnn0fiub0  12793  expcl2lem  12872  expclzlem  12884  expnegz  12894  leexp2r  12918  bcval4  13094  bccmpl  13096  hashbnd  13123  elovmpt2wrd  13347  ccatval2  13362  ccatrcl1  13376  wrdl1s1  13394  ccat2s1fvw  13415  swrdsb0eq  13447  swrdccatin1  13483  repswswrd  13531  cshwcsh2id  13574  absexpz  14045  climbdd  14402  iseraltlem2  14413  binomfallfac  14772  dvdsle  15032  divalgb  15127  ndvdssub  15133  dvdsgcd  15261  rplpwr  15276  lcmgcdlem  15319  lcmfunsn  15357  coprmdvds1  15365  qredeq  15371  prmdvdsexpr  15429  nnnn0modprm0  15511  prm23ge5  15520  pcexp  15564  difsqpwdvds  15591  prmpwdvds  15608  ramcl  15733  cshwshashlem3  15804  cshwrepswhash1  15809  elrestr  16089  xpscfv  16222  mreintcl  16255  mremre  16264  mrieqv2d  16299  initoeu2lem1  16664  funcestrcsetclem9  16788  funcsetcestrclem9  16803  prstr  16933  drsdirfi  16938  latnlej  17068  latnlej2  17071  acsdrsel  17167  acsdrscl  17170  mrelatglb  17184  mrelatlub  17186  isnmgm  17246  grpasscan1  17478  grpinvnz  17486  mulgneg2  17575  gsmsymgrfix  17848  f1omvdco2  17868  symggen  17890  odcl2  17982  odhash3  17991  lsmss1  18079  lsmss2  18081  efgred  18161  efgcpbl  18169  ablfacrp  18465  ablfac1eu  18472  ablfaclem3  18486  dvdsrmul1  18653  dvdsunit  18663  irredmul  18709  lmodlema  18868  ply1scln0  19661  psgnodpmr  19936  lindsss  20163  lindfmm  20166  dmatelnd  20302  mdetdiaglem  20404  mdet0  20412  mdetunilem7  20424  slesolinv  20486  cramerimplem3  20491  cpmatpmat  20515  m2cpminvid2lem  20559  chfacfscmul0  20663  chfacfpmmul0  20667  riinopn  20713  clsndisj  20879  cnpf2  21054  hausnei2  21157  cmpcov  21192  cmpfii  21212  unconn  21232  t1connperf  21239  nrmr0reg  21552  fbfinnfr  21645  filuni  21689  alexsubALT  21855  tmdgsum  21899  cuspcvg  22105  mopni  22297  isngp4  22416  metdsre  22656  iimulcl  22736  phtpc01  22796  clmmulg  22901  cfilucfil4  23118  bcthlem5  23125  bcth  23126  bcth3  23128  itg1le  23480  itg2le  23506  bddmulibl  23605  dvnres  23694  cpnord  23698  dvnfre  23715  deg1ge  23858  dgr1term  24016  aaliou3lem2  24098  sincosq1lem  24249  cxpge0  24429  cxpmul2  24435  logrec  24501  sqfpc  24863  bcmono  25002  gausslemma2dlem1a  25090  gausslemma2dlem2  25092  gausslemma2dlem4  25094  2lgsoddprmlem3  25139  pntrmax  25253  qabvexp  25315  ostth2lem2  25323  ax5seglem4  25812  axeuclidlem  25842  uhgredgrnv  26025  usgredg4  26109  nbuhgr2vtx1edgblem  26247  vtxduhgr0e  26374  vtxduhgr0nedg  26388  rusgrpropnb  26479  uspgr2wlkeqi  26544  redwlklem  26568  lfgrwlkprop  26584  2pthnloop  26627  spthonepeq  26648  pthdlem2lem  26663  crctcshwlkn0lem3  26704  crctcshwlkn0lem5  26706  crctcshwlkn0lem7  26708  crctcshwlkn0  26713  wlkiswwlks1  26753  wlkiswwlks2  26761  wlkiswwlksupgr2  26763  wwlksnext  26788  wwlksnextproplem2  26805  wspthsnonn0vne  26813  2pthon3v  26839  rusgrnumwwlk  26870  wwlksext2clwwlk  26924  erclwwlkseqlen  26933  erclwwlkssym  26935  erclwwlkstr  26936  erclwwlksneqlen  26945  erclwwlksnsym  26947  erclwwlksntr  26948  uhgr3cyclex  27042  upgreupthseg  27069  eupth2lem3lem4  27091  eucrctshift  27103  4cycl2vnunb  27154  nvs  27518  nvtri  27525  nmlno0  27650  nmlnoubi  27651  ubth  27729  hlipgt0  27770  ocnel  28157  elspansn2  28426  elspansn3  28431  normcan  28435  pjoml2  28470  lecm  28476  osum  28504  nmbdfnlb  28909  leopmul  28993  hstpyth  29088  cvnbtwn  29145  ssmd1  29170  ssmd2  29171  ssdmd1  29172  ssdmd2  29173  cvmd  29195  cvdmd  29196  superpos  29213  disji2f  29390  disjif  29391  disjif2  29394  padct  29497  ffs2  29503  bcm1n  29554  omndadd  29706  ogrpaddlt  29718  archiabl  29752  slmdlema  29756  eulerpartlemb  30430  sgn3da  30603  cvmsdisj  31252  cvmlift2lem12  31296  br1steqgOLD  31674  br2ndeqgOLD  31675  poseq  31750  nosepon  31818  nolesgn2o  31824  nosepnelem  31830  nosepne  31831  nosepdmlem  31833  nosepdm  31834  nodenselem8  31841  noresle  31846  noetalem3  31865  sslttr  31914  scutbdaylt  31922  lineintmo  32264  nn0prpwlem  32317  nn0prpw  32318  neibastop2lem  32355  bddiblnc  33480  areacirc  33505  incsequz  33544  mettrifi  33553  ismtybnd  33606  heiborlem1  33610  rngoisocnv  33780  risci  33786  lfl1  34357  lkrlsp2  34390  omlfh3N  34546  cvrnbtwn  34558  cvrnbtwn2  34562  cvrnbtwn4  34566  cvlexch3  34619  cvlexch4N  34620  cvlatexchb1  34621  2llnne2N  34694  atcvrj0  34714  cvrat2  34715  ps-1  34763  3atlem5  34773  islln2a  34803  lplnriaN  34836  lplnribN  34837  llncvrlpln2  34843  lplncvrlvol2  34901  psubatN  35041  pmapglb2N  35057  pmapglb2xN  35058  2llnma1b  35072  paddasslem17  35122  pmod2iN  35135  pmodl42N  35137  hlmod1i  35142  atmod1i1  35143  atmod1i2  35145  llnmod1i2  35146  pclcmpatN  35187  osumcllem8N  35249  pexmidlem3N  35258  pl42lem4N  35268  4atexlem7  35361  ltrnnid  35422  cdlemc4  35481  cdleme32a  35729  cdlemeg46gfre  35820  cdlemf2  35850  cdlemg4c  35900  trlcoat  36011  tendovalco  36053  tendoeq2  36062  cdlemk36  36201  diael  36332  diatrl  36333  dicelval1stN  36477  dicelval2nd  36478  dihlspsnat  36622  dochkr1  36767  lcfrlem9  36839  mapdh8e  37073  hdmapval0  37125  hgmapval0  37184  incssnn0  37274  pell14qrexpcl  37431  pell14qrgap  37439  congadd  37533  acongsym  37543  acongtr  37545  dvdsacongtr  37551  jm2.19lem3  37558  jm2.19lem4  37559  jm2.26lem3  37568  relexpiidm  37996  bi13impia  38694  3impcombi  39044  ioogtlb  39717  iocgtlb  39724  iocleub  39725  icoltub  39732  iooltub  39735  limclner  39883  limsupre3lem  39964  climuzlem  39975  elfzelfzlble  41331  subsubelfzo0  41336  iccpartigtl  41359  pfx2  41412  pfxccatpfx2  41428  sqrtpwpw2p  41450  fmtnoprmfac1lem  41476  fmtno4prmfac  41484  evenltle  41626  even3prm2  41628  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  bgoldbtbndlem1  41693  bgoldbtbndlem3  41695  bgoldbtbndlem4  41696  bgoldbtbnd  41697  upgrwlkupwlk  41721  c0snmgmhm  41914  funcringcsetcALTV2lem9  42044  funcringcsetclem9ALTV  42067  lincscmcl  42221  lindslinindimp2lem4  42250  lincresunit2  42267  lincresunit3  42270  elfzolborelfzop1  42309  m1modmmod  42316  rege1logbzge0  42353  fllog2  42362  dignn0ldlem  42396