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

Theorem 3impia 1193
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
StepHypRef Expression
1 3impia.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
21ex 434 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1190 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  mopick2  2370  3gencl  3145  mob2  3283  moi  3286  reupick3  3783  disjne  3872  disji2  4434  disji  4435  tz7.2  4863  ordintdif  4927  sofld  5455  funopg  5620  fvun1  5938  fvopab6  5974  fvcofneq  6029  fprg  6070  isores3  6219  ovmpt4g  6409  ovmpt2s  6410  ov2gf  6411  suppss2OLD  6514  ofrval  6534  sorpssuni  6573  sorpssint  6574  poxp  6895  suppss2  6934  smoel  7031  smoord  7036  smogt  7038  oaass  7210  oewordi  7240  oeoalem  7245  oeoelem  7247  nnawordi  7270  nnaass  7271  qsel  7390  xpdom3  7615  onsdominel  7666  mapdom3  7689  fisseneq  7731  cantnflem1  8108  cantnflem1OLD  8131  cfslbn  8647  cfsmolem  8650  cfcoflem  8652  infpssrlem4  8686  fin23lem7  8696  fin23lem25  8704  isf34lem7  8759  hsmexlem2  8807  axcc3  8818  axdc4lem  8835  tskss  9136  gruss  9174  gruurn  9176  gruiun  9177  gruel  9181  gruen  9190  grudomon  9195  grothac  9208  axpre-sup  9546  axsup  9660  letrp1  10384  p1le  10385  lemul1a  10396  zextle  10934  zextlt  10935  btwnnz  10937  gtndiv  10938  uzind2  10953  fzind  10959  eluzsub  11111  zsupss  11171  xrltne  11366  qbtwnre  11398  qbtwnxr  11399  xlemul1a  11480  iccleub  11580  iccsplit  11653  uzsubsubfz  11707  elfz0fzfz0  11777  difelfznle  11786  elfzo0le  11834  fzonmapblen  11836  fzofzim  11837  fzosplitprm1  11887  ceile  11944  modadd1  12001  modmul1  12008  modirr  12025  fsuppmapnn0fiub0  12067  expcl2lem  12146  expclzlem  12158  expnegz  12168  leexp2r  12191  bcval4  12353  bccmpl  12355  hashbnd  12379  elovmpt2wrd  12548  ccatval2  12561  wrdl1s1  12585  swrdccatin1  12671  repswswrd  12719  cshwcsh2id  12759  absexpz  13101  climbdd  13457  iseraltlem2  13468  znnenlem  13806  dvdsle  13890  divalgb  13921  ndvdssub  13924  dvdsgcd  14040  rplpwr  14053  qredeq  14106  prmdvdsexpr  14116  nnnn0modprm0  14190  pcexp  14242  prmpwdvds  14281  ramcl  14406  cshwshashlem3  14440  cshwrepswhash1  14445  elrestr  14684  xpscfv  14817  mreintcl  14850  mremre  14859  mrieqv2d  14894  prstr  15420  drsdirfi  15425  latnlej  15555  latnlej2  15558  acsdrsel  15654  acsdrscl  15657  mrelatglb  15671  mrelatlub  15673  grpinvnz  15919  mulgneg2  15979  gsmsymgrfix  16258  f1omvdco2  16279  symggen  16301  odcl2  16393  odhash3  16402  lsmss1  16490  lsmss2  16492  efgred  16572  efgcpbl  16580  ablfacrp  16919  ablfac1eu  16926  ablfaclem3  16940  dvdsrmul1  17103  dvdsunit  17113  irredmul  17159  lmodlema  17317  ply1scln0  18131  psgnodpmr  18421  lindsss  18654  lindfmm  18657  dmatelnd  18793  mdetdiaglem  18895  mdet0  18903  mdetunilem7  18915  slesolinv  18977  cramerimplem3  18982  cpmatpmat  19006  m2cpminvid2lem  19050  chfacfscmul0  19154  chfacfpmmul0  19158  riinopn  19212  clsndisj  19370  cnpf2  19545  hausnei2  19648  cmpcov  19683  cmpfii  19703  bwthOLD  19705  uncon  19724  t1conperf  19731  nrmr0reg  20013  fbfinnfr  20105  filuni  20149  alexsubALT  20314  tmdgsum  20357  cuspcvg  20567  mopni  20758  isngp4  20894  metdsre  21120  iimulcl  21200  phtpc01  21259  clmmulg  21356  cfilucfil4OLD  21522  cfilucfil4  21523  bcthlem5  21530  bcth  21531  bcth3  21533  itg1le  21883  itg2le  21909  bddmulibl  22008  dvnres  22097  cpnord  22101  dvnfre  22118  deg1ge  22262  dgr1term  22419  aaliou3lem2  22501  sincosq1lem  22651  cxpge0  22820  cxpmul2  22826  logrec  22907  sqfpc  23167  bcmono  23308  pntrmax  23505  qabvexp  23567  ostth2lem2  23575  ax5seglem4  23939  axeuclidlem  23969  edgwlk  24235  usgra2wlkspthlem1  24323  usgra2wlkspthlem2  24324  wwlknimp  24391  wlkiswwlk1  24394  wlkiswwlk2  24401  wwlknext  24428  wwlkextproplem2  24446  wwlkext2clwwlk  24507  erclwwlkeqlen  24516  erclwwlksym  24518  erclwwlktr  24519  erclwwlkneqlen  24528  erclwwlknsym  24530  erclwwlkntr  24531  usg2wotspth  24588  usgfiregdegfi  24615  rusgraprop2  24646  rusgraprop3  24647  rusgranumwlk  24661  4cycl2vnunb  24721  usgn0fidegnn0  24734  grpoasscan1  24943  gxnn0neg  24969  gxnn0suc  24970  gxcl  24971  gxneg  24972  gxcom  24975  gxinv  24976  gxsuc  24978  gxnn0add  24980  gxadd  24981  gxnn0mul  24983  gxmul  24984  gxdi  25002  nvs  25269  nvtri  25277  nmlno0  25414  nmlnoubi  25415  ubth  25493  hlipgt0  25534  ocnel  25920  elspansn2  26189  elspansn3  26194  normcan  26198  pjoml2  26233  lecm  26239  osum  26267  nmbdfnlb  26673  leopmul  26757  hstpyth  26852  cvnbtwn  26909  ssmd1  26934  ssmd2  26935  ssdmd1  26936  ssdmd2  26937  cvmd  26959  cvdmd  26960  superpos  26977  disji2f  27139  disjif  27140  disjif2  27143  bcm1n  27296  omndadd  27386  ogrpaddlt  27398  archiabl  27432  slmdlema  27436  eulerpartlemb  27975  sgn3da  28148  cvmsdisj  28383  cvmlift2lem12  28427  binomfallfac  28768  poseq  28938  nodenselem8  29053  nofulllem4  29070  lineintmo  29412  bddiblnc  29690  areacirc  29717  nn0prpwlem  29745  nn0prpw  29746  neibastop2lem  29809  incsequz  29872  mettrifi  29881  ismtybnd  29934  heiborlem1  29938  rngoisocnv  30015  risci  30021  incssnn0  30275  pell14qrexpcl  30435  pell14qrgap  30443  congadd  30536  acongsym  30546  acongtr  30548  dvdsacongtr  30554  jm2.19lem3  30565  jm2.19lem4  30566  jm2.26lem3  30575  lcmgcdlem  30840  ioogtlb  31120  iocgtlb  31127  iocleub  31128  icogelb  31134  icoltub  31137  iooltub  31140  iblspltprt  31319  2f1fvneq  31802  elfzelfzlble  31832  subsubelfzo0  31833  el2fzo  31834  usgra2pthspth  31846  lincscmcl  32132  lindslinindimp2lem4  32161  lincresunit2  32178  lincresunit3  32181  bi13impia  32354  3impcombi  32712  lfl1  33885  lkrlsp2  33918  omlfh3N  34074  cvrnbtwn  34086  cvrnbtwn2  34090  cvrnbtwn4  34094  cvlexch3  34147  cvlexch4N  34148  cvlatexchb1  34149  2llnne2N  34222  atcvrj0  34242  cvrat2  34243  ps-1  34291  3atlem5  34301  islln2a  34331  lplnriaN  34364  lplnribN  34365  llncvrlpln2  34371  lplncvrlvol2  34429  psubatN  34569  pmapglb2N  34585  pmapglb2xN  34586  2llnma1b  34600  paddasslem17  34650  pmod2iN  34663  pmodl42N  34665  hlmod1i  34670  atmod1i1  34671  atmod1i2  34673  llnmod1i2  34674  pclcmpatN  34715  osumcllem8N  34777  pexmidlem3N  34786  pl42lem4N  34796  4atexlem7  34889  ltrnnid  34950  cdlemc4  35008  cdleme32a  35255  cdlemeg46gfre  35346  cdlemf2  35376  cdlemg4c  35426  trlcoat  35537  tendovalco  35579  tendoeq2  35588  cdlemk36  35727  diael  35858  diatrl  35859  dicelval1stN  36003  dicelval2nd  36004  dihlspsnat  36148  dochkr1  36293  lcfrlem9  36365  mapdh8e  36599  hdmapval0  36651  hgmapval0  36710
  Copyright terms: Public domain W3C validator