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

Theorem 3impia 1194
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 1191 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
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 976
This theorem is referenced by:  mopick2  2348  3gencl  3127  mob2  3265  moi  3268  reupick3  3768  disjne  3858  disji2  4424  disji  4425  tz7.2  4853  ordintdif  4917  sofld  5445  funopg  5610  fvun1  5929  fvopab6  5965  fveqressseq  6012  fvcofneq  6024  fprg  6065  isores3  6216  ovmpt4g  6410  ovmpt2s  6411  ov2gf  6412  suppss2OLD  6515  ofrval  6535  sorpssuni  6574  sorpssint  6575  poxp  6897  suppss2  6936  smoel  7033  smoord  7038  smogt  7040  oaass  7212  oewordi  7242  oeoalem  7247  oeoelem  7249  nnawordi  7272  nnaass  7273  qsel  7392  xpdom3  7617  onsdominel  7668  mapdom3  7691  fisseneq  7733  cantnflem1  8111  cantnflem1OLD  8134  cfslbn  8650  cfsmolem  8653  cfcoflem  8655  infpssrlem4  8689  fin23lem7  8699  fin23lem25  8707  isf34lem7  8762  hsmexlem2  8810  axcc3  8821  axdc4lem  8838  tskss  9139  gruss  9177  gruurn  9179  gruiun  9180  gruel  9184  gruen  9193  grudomon  9198  grothac  9211  axpre-sup  9549  axsup  9663  letrp1  10390  p1le  10391  lemul1a  10402  zextle  10942  zextlt  10943  btwnnz  10945  gtndiv  10946  uzind2  10961  fzind  10967  eluzsub  11119  zsupss  11180  xrltne  11375  qbtwnre  11407  qbtwnxr  11408  xlemul1a  11489  iccleub  11589  iccsplit  11662  uzsubsubfz  11716  elfz0fzfz0  11787  difelfznle  11797  elfzo0le  11845  fzonmapblen  11847  fzofzim  11848  fzosplitprm1  11898  ceile  11955  modadd1  12012  modmul1  12019  modirr  12036  fsuppmapnn0fiub0  12078  expcl2lem  12157  expclzlem  12169  expnegz  12179  leexp2r  12202  bcval4  12364  bccmpl  12366  hashbnd  12390  elovmpt2wrd  12562  ccatval2  12575  wrdl1s1  12601  swrdccatin1  12687  repswswrd  12735  cshwcsh2id  12775  absexpz  13117  climbdd  13473  iseraltlem2  13484  znnenlem  13822  dvdsle  13908  divalgb  13939  ndvdssub  13942  dvdsgcd  14058  rplpwr  14071  qredeq  14124  prmdvdsexpr  14134  nnnn0modprm0  14208  pcexp  14260  prmpwdvds  14299  ramcl  14424  cshwshashlem3  14459  cshwrepswhash1  14464  elrestr  14703  xpscfv  14836  mreintcl  14869  mremre  14878  mrieqv2d  14913  prstr  15436  drsdirfi  15441  latnlej  15572  latnlej2  15575  acsdrsel  15671  acsdrscl  15674  mrelatglb  15688  mrelatlub  15690  isnmgm  15750  mndassOLD  15806  grpinvnz  15983  mulgneg2  16043  gsmsymgrfix  16327  f1omvdco2  16347  symggen  16369  odcl2  16461  odhash3  16470  lsmss1  16558  lsmss2  16560  efgred  16640  efgcpbl  16648  ablfacrp  16991  ablfac1eu  16998  ablfaclem3  17012  dvdsrmul1  17176  dvdsunit  17186  irredmul  17232  lmodlema  17391  ply1scln0  18206  psgnodpmr  18499  lindsss  18732  lindfmm  18735  dmatelnd  18871  mdetdiaglem  18973  mdet0  18981  mdetunilem7  18993  slesolinv  19055  cramerimplem3  19060  cpmatpmat  19084  m2cpminvid2lem  19128  chfacfscmul0  19232  chfacfpmmul0  19236  riinopn  19290  clsndisj  19449  cnpf2  19624  hausnei2  19727  cmpcov  19762  cmpfii  19782  bwthOLD  19784  uncon  19803  t1conperf  19810  nrmr0reg  20123  fbfinnfr  20215  filuni  20259  alexsubALT  20424  tmdgsum  20467  cuspcvg  20677  mopni  20868  isngp4  21004  metdsre  21230  iimulcl  21310  phtpc01  21369  clmmulg  21466  cfilucfil4OLD  21632  cfilucfil4  21633  bcthlem5  21640  bcth  21641  bcth3  21643  itg1le  21993  itg2le  22019  bddmulibl  22118  dvnres  22207  cpnord  22211  dvnfre  22228  deg1ge  22372  dgr1term  22529  aaliou3lem2  22611  sincosq1lem  22762  cxpge0  22936  cxpmul2  22942  logrec  23023  sqfpc  23283  bcmono  23424  pntrmax  23621  qabvexp  23683  ostth2lem2  23691  ax5seglem4  24107  axeuclidlem  24137  edgwlk  24403  usgra2wlkspthlem1  24491  usgra2wlkspthlem2  24492  wwlknimp  24559  wlkiswwlk1  24562  wlkiswwlk2  24569  wwlknext  24596  wwlkextproplem2  24614  wwlkext2clwwlk  24675  erclwwlkeqlen  24684  erclwwlksym  24686  erclwwlktr  24687  erclwwlkneqlen  24696  erclwwlknsym  24698  erclwwlkntr  24699  usg2wotspth  24756  usgfiregdegfi  24783  rusgraprop2  24814  rusgraprop3  24815  rusgranumwlk  24829  4cycl2vnunb  24889  usgn0fidegnn0  24901  grpoasscan1  25111  gxnn0neg  25137  gxnn0suc  25138  gxcl  25139  gxneg  25140  gxcom  25143  gxinv  25144  gxsuc  25146  gxnn0add  25148  gxadd  25149  gxnn0mul  25151  gxmul  25152  gxdi  25170  nvs  25437  nvtri  25445  nmlno0  25582  nmlnoubi  25583  ubth  25661  hlipgt0  25702  ocnel  26088  elspansn2  26357  elspansn3  26362  normcan  26366  pjoml2  26401  lecm  26407  osum  26435  nmbdfnlb  26841  leopmul  26925  hstpyth  27020  cvnbtwn  27077  ssmd1  27102  ssmd2  27103  ssdmd1  27104  ssdmd2  27105  cvmd  27127  cvdmd  27128  superpos  27145  disji2f  27310  disjif  27311  disjif2  27314  ffs2  27423  bcm1n  27472  omndadd  27569  ogrpaddlt  27581  archiabl  27615  slmdlema  27619  eulerpartlemb  28180  sgn3da  28353  cvmsdisj  28588  cvmlift2lem12  28632  binomfallfac  29138  poseq  29308  nodenselem8  29423  nofulllem4  29440  lineintmo  29782  bddiblnc  30060  areacirc  30087  nn0prpwlem  30115  nn0prpw  30116  neibastop2lem  30153  incsequz  30216  mettrifi  30225  ismtybnd  30278  heiborlem1  30282  rngoisocnv  30359  risci  30365  incssnn0  30618  pell14qrexpcl  30778  pell14qrgap  30786  congadd  30879  acongsym  30889  acongtr  30891  dvdsacongtr  30897  jm2.19lem3  30908  jm2.19lem4  30909  jm2.26lem3  30918  lcmgcdlem  31188  ioogtlb  31464  iocgtlb  31471  iocleub  31472  icogelb  31478  icoltub  31481  iooltub  31484  limclner  31565  2f1fvneq  32145  elfzelfzlble  32175  subsubelfzo0  32176  el2fzo  32177  usgra2pthspth  32189  funcestrcsetclem9  32500  funcringcsetcOLD2lem9  32584  funcringcsetclem9OLD  32607  lincscmcl  32763  lindslinindimp2lem4  32792  lincresunit2  32809  lincresunit3  32812  bi13impia  32985  3impcombi  33342  lfl1  34529  lkrlsp2  34562  omlfh3N  34718  cvrnbtwn  34730  cvrnbtwn2  34734  cvrnbtwn4  34738  cvlexch3  34791  cvlexch4N  34792  cvlatexchb1  34793  2llnne2N  34866  atcvrj0  34886  cvrat2  34887  ps-1  34935  3atlem5  34945  islln2a  34975  lplnriaN  35008  lplnribN  35009  llncvrlpln2  35015  lplncvrlvol2  35073  psubatN  35213  pmapglb2N  35229  pmapglb2xN  35230  2llnma1b  35244  paddasslem17  35294  pmod2iN  35307  pmodl42N  35309  hlmod1i  35314  atmod1i1  35315  atmod1i2  35317  llnmod1i2  35318  pclcmpatN  35359  osumcllem8N  35421  pexmidlem3N  35430  pl42lem4N  35440  4atexlem7  35533  ltrnnid  35594  cdlemc4  35653  cdleme32a  35901  cdlemeg46gfre  35992  cdlemf2  36022  cdlemg4c  36072  trlcoat  36183  tendovalco  36225  tendoeq2  36234  cdlemk36  36373  diael  36504  diatrl  36505  dicelval1stN  36649  dicelval2nd  36650  dihlspsnat  36794  dochkr1  36939  lcfrlem9  37011  mapdh8e  37245  hdmapval0  37297  hgmapval0  37356
  Copyright terms: Public domain W3C validator