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

Theorem 3impia 1202
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 435 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1199 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  mopick2  2339  3gencl  3113  mob2  3250  moi  3253  reupick3  3758  disjne  3840  disji2  4410  disji  4411  tz7.2  4837  sofld  5303  ordintdif  5491  funopg  5633  fvun1  5952  fvopab6  5990  fveqressseq  6033  fvcofneq  6045  fprg  6088  isores3  6241  ovmpt4g  6433  ovmpt2s  6434  ov2gf  6435  ofrval  6555  sorpssuni  6594  sorpssint  6595  poxp  6919  suppss2  6960  smoel  7090  smoord  7095  smogt  7097  oaass  7273  oewordi  7303  oeoalem  7308  oeoelem  7310  nnawordi  7333  nnaass  7334  qsel  7453  xpdom3  7679  onsdominel  7730  mapdom3  7753  fisseneq  7792  cantnflem1  8202  cfslbn  8704  cfsmolem  8707  cfcoflem  8709  infpssrlem4  8743  fin23lem7  8753  fin23lem25  8761  isf34lem7  8816  hsmexlem2  8864  axcc3  8875  axdc4lem  8892  tskss  9190  gruss  9228  gruurn  9230  gruiun  9231  gruel  9235  gruen  9244  grudomon  9249  grothac  9262  axpre-sup  9600  axsup  9716  letrp1  10454  p1le  10455  lemul1a  10466  infrelb  10603  zextle  11016  zextlt  11017  btwnnz  11019  gtndiv  11020  uzind2  11035  fzind  11040  eluzsub  11195  zsupss  11260  xrltne  11467  qbtwnre  11499  qbtwnxr  11500  xlemul1a  11581  icogelb  11693  iccleub  11697  iccsplit  11772  uzsubsubfz  11828  elfz0fzfz0  11902  difelfznle  11912  elfzo0le  11966  fzonmapblen  11968  fzofzim  11969  fzosplitprm1  12024  ceile  12082  modadd1  12140  muladdmodid  12143  modmul1  12149  modirr  12166  fsuppmapnn0fiub0  12211  expcl2lem  12290  expclzlem  12302  expnegz  12312  leexp2r  12336  bcval4  12498  bccmpl  12500  hashbnd  12527  elovmpt2wrd  12713  ccatval2  12727  wrdl1s1  12753  ccat2s1fvw  12773  swrdsb0eq  12805  swrdccatin1  12841  repswswrd  12889  cshwcsh2id  12929  absexpz  13368  climbdd  13734  iseraltlem2  13748  binomfallfac  14093  znnenlem  14263  dvdsle  14349  divalgb  14384  ndvdssub  14387  dvdsgcd  14510  rplpwr  14523  lcmgcdlem  14570  lcmfunsn  14616  qredeq  14662  prmdvdsexpr  14668  nnnn0modprm0  14756  pcexp  14808  prmpwdvds  14847  ramcl  14986  cshwshashlem3  15067  cshwrepswhash1  15072  elrestr  15326  xpscfv  15467  mreintcl  15500  mremre  15509  mrieqv2d  15544  initoeu2lem1  15908  funcestrcsetclem9  16032  funcsetcestrclem9  16047  prstr  16177  drsdirfi  16182  latnlej  16313  latnlej2  16316  acsdrsel  16412  acsdrscl  16415  mrelatglb  16429  mrelatlub  16431  isnmgm  16491  mndassOLD  16547  grpinvnz  16724  mulgneg2  16784  gsmsymgrfix  17068  f1omvdco2  17088  symggen  17110  odcl2  17215  odhash3  17224  lsmss1  17315  lsmss2  17317  efgred  17397  efgcpbl  17405  ablfacrp  17698  ablfac1eu  17705  ablfaclem3  17719  dvdsrmul1  17880  dvdsunit  17890  irredmul  17936  lmodlema  18095  ply1scln0  18883  psgnodpmr  19156  lindsss  19380  lindfmm  19383  dmatelnd  19519  mdetdiaglem  19621  mdet0  19629  mdetunilem7  19641  slesolinv  19703  cramerimplem3  19708  cpmatpmat  19732  m2cpminvid2lem  19776  chfacfscmul0  19880  chfacfpmmul0  19884  riinopn  19936  clsndisj  20089  cnpf2  20264  hausnei2  20367  cmpcov  20402  cmpfii  20422  uncon  20442  t1conperf  20449  nrmr0reg  20762  fbfinnfr  20854  filuni  20898  alexsubALT  21064  tmdgsum  21108  cuspcvg  21314  mopni  21505  isngp4  21623  metdsre  21868  metdsreOLD  21883  iimulcl  21963  phtpc01  22025  clmmulg  22122  cfilucfil4  22287  bcthlem5  22294  bcth  22295  bcth3  22297  itg1le  22669  itg2le  22695  bddmulibl  22794  dvnres  22883  cpnord  22887  dvnfre  22904  deg1ge  23045  dgr1term  23212  aaliou3lem2  23297  sincosq1lem  23450  cxpge0  23626  cxpmul2  23632  logrec  23698  sqfpc  24062  bcmono  24203  pntrmax  24400  qabvexp  24462  ostth2lem2  24470  ax5seglem4  24960  axeuclidlem  24990  edgwlk  25257  usgra2wlkspthlem1  25345  usgra2wlkspthlem2  25346  wwlknimp  25413  wlkiswwlk1  25416  wlkiswwlk2  25423  wwlknext  25450  wwlkextproplem2  25468  wwlkext2clwwlk  25529  erclwwlkeqlen  25538  erclwwlksym  25540  erclwwlktr  25541  erclwwlkneqlen  25550  erclwwlknsym  25552  erclwwlkntr  25553  usg2wotspth  25610  usgfiregdegfi  25637  rusgraprop2  25668  rusgraprop3  25669  rusgranumwlk  25683  4cycl2vnunb  25743  usgn0fidegnn0  25755  grpoasscan1  25963  gxnn0neg  25989  gxnn0suc  25990  gxcl  25991  gxneg  25992  gxcom  25995  gxinv  25996  gxsuc  25998  gxnn0add  26000  gxadd  26001  gxnn0mul  26003  gxmul  26004  gxdi  26022  nvs  26289  nvtri  26297  nmlno0  26434  nmlnoubi  26435  ubth  26513  hlipgt0  26564  ocnel  26949  elspansn2  27218  elspansn3  27223  normcan  27227  pjoml2  27262  lecm  27268  osum  27296  nmbdfnlb  27701  leopmul  27785  hstpyth  27880  cvnbtwn  27937  ssmd1  27962  ssmd2  27963  ssdmd1  27964  ssdmd2  27965  cvmd  27987  cvdmd  27988  superpos  28005  disji2f  28189  disjif  28190  disjif2  28193  padct  28313  ffs2  28319  bcm1n  28377  omndadd  28476  ogrpaddlt  28488  archiabl  28522  slmdlema  28526  eulerpartlemb  29209  sgn3da  29420  cvmsdisj  30001  cvmlift2lem12  30045  br1steqg  30423  br2ndeqg  30424  poseq  30498  nodenselem8  30582  nofulllem4  30599  lineintmo  30929  nn0prpwlem  30983  nn0prpw  30984  neibastop2lem  31021  bddiblnc  31976  areacirc  32001  incsequz  32041  mettrifi  32050  ismtybnd  32103  heiborlem1  32107  rngoisocnv  32184  risci  32190  lfl1  32605  lkrlsp2  32638  omlfh3N  32794  cvrnbtwn  32806  cvrnbtwn2  32810  cvrnbtwn4  32814  cvlexch3  32867  cvlexch4N  32868  cvlatexchb1  32869  2llnne2N  32942  atcvrj0  32962  cvrat2  32963  ps-1  33011  3atlem5  33021  islln2a  33051  lplnriaN  33084  lplnribN  33085  llncvrlpln2  33091  lplncvrlvol2  33149  psubatN  33289  pmapglb2N  33305  pmapglb2xN  33306  2llnma1b  33320  paddasslem17  33370  pmod2iN  33383  pmodl42N  33385  hlmod1i  33390  atmod1i1  33391  atmod1i2  33393  llnmod1i2  33394  pclcmpatN  33435  osumcllem8N  33497  pexmidlem3N  33506  pl42lem4N  33516  4atexlem7  33609  ltrnnid  33670  cdlemc4  33729  cdleme32a  33977  cdlemeg46gfre  34068  cdlemf2  34098  cdlemg4c  34148  trlcoat  34259  tendovalco  34301  tendoeq2  34310  cdlemk36  34449  diael  34580  diatrl  34581  dicelval1stN  34725  dicelval2nd  34726  dihlspsnat  34870  dochkr1  35015  lcfrlem9  35087  mapdh8e  35321  hdmapval0  35373  hgmapval0  35432  incssnn0  35522  pell14qrexpcl  35683  pell14qrgap  35691  congadd  35786  acongsym  35796  acongtr  35798  dvdsacongtr  35804  jm2.19lem3  35816  jm2.19lem4  35817  jm2.26lem3  35826  relexpiidm  36266  bi13impia  36814  3impcombi  37177  ioogtlb  37541  iocgtlb  37548  iocleub  37549  icoltub  37556  iooltub  37559  limclner  37672  iccpartigtl  38607  wtgoldbnnsum4prm  38767  bgoldbnnsum3prm  38769  bgoldbtbndlem1  38770  bgoldbtbndlem3  38772  bgoldbtbndlem4  38773  bgoldbtbnd  38774  pfx2  38823  pfxccatpfx2  38839  2f1fvneq  38877  elfzelfzlble  38915  subsubelfzo0  38916  usgredg4  39080  nbuhgr2vtx1edgblem  39183  usgra2pthspth  39284  c0snmgmhm  39533  funcringcsetcALTV2lem9  39665  funcringcsetclem9ALTV  39688  lincscmcl  39846  lindslinindimp2lem4  39875  lincresunit2  39892  lincresunit3  39895  elfzolborelfzop1  39937  m1modmmod  39945  rege1logbzge0  39991  fllog2  40000  dignn0ldlem  40034
  Copyright terms: Public domain W3C validator