MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3impia Unicode version

Theorem 3impia 1185
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
Hypothesis
Ref Expression
3impia.1
Assertion
Ref Expression
3impia

Proof of Theorem 3impia
StepHypRef Expression
1 3impia.1 . . 3
21ex 434 . 2
323imp 1182 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 965
This theorem is referenced by:  mopick2  2357  3gencl  3113  mob2  3249  moi  3252  reupick3  3749  disjne  3838  disji2  4396  disji  4397  tz7.2  4821  ordintdif  4885  sofld  5405  funopg  5569  fvun1  5885  fvopab6  5919  fvcofneq  5974  fprg  6015  isores3  6157  ovmpt4g  6346  ovmpt2s  6347  ov2gf  6348  suppss2OLD  6448  ofrval  6463  sorpssuni  6502  sorpssint  6503  poxp  6818  suppss2  6857  smoel  6955  smoord  6960  smogt  6962  oaass  7134  oewordi  7164  oeoalem  7169  oeoelem  7171  nnawordi  7194  nnaass  7195  qsel  7313  xpdom3  7543  onsdominel  7594  mapdom3  7617  fisseneq  7659  cantnflem1  8034  cantnflem1OLD  8057  cfslbn  8573  cfsmolem  8576  cfcoflem  8578  infpssrlem4  8612  fin23lem7  8622  fin23lem25  8630  isf34lem7  8685  hsmexlem2  8733  axcc3  8744  axdc4lem  8761  tskss  9062  gruss  9100  gruurn  9102  gruiun  9103  gruel  9107  gruen  9116  grudomon  9121  grothac  9134  axpre-sup  9473  axsup  9587  letrp1  10308  p1le  10309  lemul1a  10320  zextle  10853  zextlt  10854  btwnnz  10856  gtndiv  10857  uzind2  10872  fzind  10878  uzletr  11008  eluzsub  11029  zsupss  11083  xrltne  11276  qbtwnre  11308  qbtwnxr  11309  xlemul1a  11390  iccleub  11490  iccsplit  11563  uzsubsubfz  11616  elfz0fzfz0  11630  elfzo0le  11735  fzonmapblen  11737  fzofzim  11738  ceile  11833  modadd1  11890  modmul1  11897  modirr  11914  fsuppmapnn0fiub0  11956  expcl2lem  12034  expclzlem  12046  expnegz  12055  leexp2r  12078  bcval4  12240  bccmpl  12242  hashbnd  12266  ccatval2  12435  wrdl1s1  12459  swrdccatin1  12532  repswswrd  12580  absexpz  12952  climbdd  13307  iseraltlem2  13318  znnenlem  13652  dvdsle  13736  divalgb  13766  ndvdssub  13769  dvdsgcd  13885  rplpwr  13898  qredeq  13950  prmdvdsexpr  13960  nnnn0modprm0  14032  pcexp  14084  prmpwdvds  14123  ramcl  14248  cshwshashlem3  14282  cshwrepswhash1  14287  elrestr  14526  xpscfv  14659  mreintcl  14692  mremre  14701  mrieqv2d  14736  prstr  15262  drsdirfi  15267  latnlej  15397  latnlej2  15400  acsdrsel  15496  acsdrscl  15499  mrelatglb  15513  mrelatlub  15515  grpinvnz  15756  mulgneg2  15813  gsmsymgrfix  16092  f1omvdco2  16113  symggen  16135  odcl2  16227  odhash3  16236  lsmss1  16324  lsmss2  16326  efgred  16406  efgcpbl  16414  ablfacrp  16742  ablfac1eu  16749  ablfaclem3  16763  dvdsrmul1  16921  dvdsunit  16931  irredmul  16977  lmodlema  17129  ply1scln0  17926  psgnodpmr  18213  lindsss  18446  lindfmm  18449  dmatelnd  18586  mdetdiaglem  18672  mdet0  18680  mdetunilem7  18692  slesolinv  18754  cramerimplem3  18759  cpmatpmat  18783  m2cpminvid2lem  18827  riinopn  18920  clsndisj  19078  cnpf2  19253  hausnei2  19356  cmpcov  19391  cmpfii  19411  bwthOLD  19413  uncon  19432  t1conperf  19439  nrmr0reg  19721  fbfinnfr  19813  filuni  19857  alexsubALT  20022  tmdgsum  20065  cuspcvg  20275  mopni  20466  isngp4  20602  metdsre  20828  iimulcl  20908  phtpc01  20967  clmmulg  21064  cfilucfil4OLD  21230  cfilucfil4  21231  bcthlem5  21238  bcth  21239  bcth3  21241  itg1le  21591  itg2le  21617  bddmulibl  21716  dvnres  21805  cpnord  21809  dvnfre  21826  deg1ge  21970  dgr1term  22127  aaliou3lem2  22209  sincosq1lem  22359  cxpge0  22528  cxpmul2  22534  logrec  22615  sqfpc  22875  bcmono  23016  pntrmax  23213  qabvexp  23275  ostth2lem2  23283  ax5seglem4  23647  axeuclidlem  23677  grpoasscan1  24193  gxnn0neg  24219  gxnn0suc  24220  gxcl  24221  gxneg  24222  gxcom  24225  gxinv  24226  gxsuc  24228  gxnn0add  24230  gxadd  24231  gxnn0mul  24233  gxmul  24234  gxdi  24252  nvs  24519  nvtri  24527  nmlno0  24664  nmlnoubi  24665  ubth  24743  hlipgt0  24784  ocnel  25170  elspansn2  25439  elspansn3  25444  normcan  25448  pjoml2  25483  lecm  25489  osum  25517  nmbdfnlb  25923  leopmul  26007  hstpyth  26102  cvnbtwn  26159  ssmd1  26184  ssmd2  26185  ssdmd1  26186  ssdmd2  26187  cvmd  26209  cvdmd  26210  superpos  26227  disji2f  26389  disjif  26390  disjif2  26393  bcm1n  26540  omndadd  26630  ogrpaddlt  26642  archiabl  26676  slmdlema  26680  eulerpartlemb  27207  sgn3da  27380  cvmsdisj  27615  cvmlift2lem12  27659  binomfallfac  28000  poseq  28170  nodenselem8  28285  nofulllem4  28302  lineintmo  28644  bddiblnc  28922  areacirc  28949  nn0prpwlem  28977  nn0prpw  28978  neibastop2lem  29041  incsequz  29104  mettrifi  29113  ismtybnd  29166  heiborlem1  29170  rngoisocnv  29247  risci  29253  incssnn0  29507  pell14qrexpcl  29668  pell14qrgap  29676  congadd  29769  acongsym  29779  acongtr  29781  dvdsacongtr  29787  jm2.19lem3  29800  jm2.19lem4  29801  jm2.26lem3  29810  ioogtlb  30321  iocgtlb  30328  iocleub  30329  icogelb  30335  icoltub  30338  iooltub  30341  iblspltprt  30520  2f1fvneq  31020  uzuzle  31067  elfzelfzlble  31086  subsubelfzo0  31087  el2fzo  31089  fzosplitprm1  31101  elovmpt2wrd  31133  edgwlk  31171  usgra2pthspth  31172  usgra2wlkspthlem1  31173  usgra2wlkspthlem2  31174  wwlknimp  31198  wlkiswwlk1  31201  wlkiswwlk2  31208  wwlknext  31233  usg2wotspth  31280  wwlkext2clwwlk  31342  erclwwlktr0  31356  erclwwlkeqlen  31359  erclwwlksym  31361  erclwwlktr  31362  difelfznle  31365  erclwwlkneqlen  31375  erclwwlknsym  31377  erclwwlkntr  31378  usgfiregdegfi  31405  rusgraprop2  31431  rusgraprop3  31432  wwlkextproplem2  31438  rusgranumwlk  31452  4cycl2vnunb  31486  usgn0fidegnn0  31499  lincscmcl  31738  lindslinindimp2lem4  31767  lincresunit2  31784  lincresunit3  31787  chfacfscmul0  31856  chfacfpmmul0  31860  bi13impia  32035  3impcombi  32393  lfl1  33566  lkrlsp2  33599  omlfh3N  33755  cvrnbtwn  33767  cvrnbtwn2  33771  cvrnbtwn4  33775  cvlexch3  33828  cvlexch4N  33829  cvlatexchb1  33830  2llnne2N  33903  atcvrj0  33923  cvrat2  33924  ps-1  33972  3atlem5  33982  islln2a  34012  lplnriaN  34045  lplnribN  34046  llncvrlpln2  34052  lplncvrlvol2  34110  psubatN  34250  pmapglb2N  34266  pmapglb2xN  34267  2llnma1b  34281  paddasslem17  34331  pmod2iN  34344  pmodl42N  34346  hlmod1i  34351  atmod1i1  34352  atmod1i2  34354  llnmod1i2  34355  pclcmpatN  34396  osumcllem8N  34458  pexmidlem3N  34467  pl42lem4N  34477  4atexlem7  34570  ltrnnid  34631  cdlemc4  34689  cdleme32a  34936  cdlemeg46gfre  35027  cdlemf2  35057  cdlemg4c  35107  trlcoat  35218  tendovalco  35260  tendoeq2  35269  cdlemk36  35408  diael  35539  diatrl  35540  dicelval1stN  35684  dicelval2nd  35685  dihlspsnat  35829  dochkr1  35974  lcfrlem9  36046  mapdh8e  36280  hdmapval0  36332  hgmapval0  36391
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 185  df-an 371  df-3an 967
  Copyright terms: Public domain W3C validator