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

Theorem 3impia 1228
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 441 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1224 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  mopick2  2389  3gencl  3065  mob2  3206  moi  3209  reupick3  3719  disjne  3814  disji2  4382  disji  4383  tz7.2  4823  sofld  5290  ordintdif  5479  funopg  5621  fvun1  5951  fvopab6  5990  fveqressseq  6033  fvcofneq  6045  fprg  6089  isores3  6244  ovmpt4g  6438  ovmpt2s  6439  ov2gf  6440  ofrval  6560  sorpssuni  6599  sorpssint  6600  poxp  6927  suppss2  6968  smoel  7097  smoord  7102  smogt  7104  oaass  7280  oewordi  7310  oeoalem  7315  oeoelem  7317  nnawordi  7340  nnaass  7341  qsel  7460  xpdom3  7688  onsdominel  7739  mapdom3  7762  fisseneq  7801  cantnflem1  8212  cfslbn  8715  cfsmolem  8718  cfcoflem  8720  infpssrlem4  8754  fin23lem7  8764  fin23lem25  8772  isf34lem7  8827  hsmexlem2  8875  axcc3  8886  axdc4lem  8903  tskss  9201  gruss  9239  gruurn  9241  gruiun  9242  gruel  9246  gruen  9255  grudomon  9260  grothac  9273  axpre-sup  9611  axsup  9727  addn0nid  10061  letrp1  10469  p1le  10470  lemul1a  10481  infrelb  10618  zextle  11032  zextlt  11033  btwnnz  11035  gtndiv  11036  uzind2  11051  fzind  11056  eluzsub  11212  zsupss  11276  xrltne  11483  qbtwnre  11515  qbtwnxr  11516  xlemul1a  11599  icogelb  11711  iccleub  11715  iccsplit  11791  uzsubsubfz  11847  elfz0fzfz0  11921  difelfznle  11930  fvffz0  11934  elfzo0le  11987  fzonmapblen  11989  fzofzim  11990  fzosplitprm1  12049  ceile  12109  modadd1  12167  muladdmodid  12170  modmul1  12177  modirr  12194  fsuppmapnn0fiub0  12243  expcl2lem  12322  expclzlem  12334  expnegz  12344  leexp2r  12368  bcval4  12530  bccmpl  12532  hashbnd  12559  elovmpt2wrd  12760  ccatval2  12774  ccatrcl1  12788  wrdl1s1  12805  ccat2s1fvw  12825  swrdsb0eq  12857  swrdccatin1  12893  repswswrd  12941  cshwcsh2id  12984  absexpz  13445  climbdd  13812  iseraltlem2  13826  binomfallfac  14171  znnenlem  14341  dvdsle  14427  divalgb  14464  ndvdssub  14467  dvdsgcd  14590  rplpwr  14603  lcmgcdlem  14650  lcmfunsn  14696  qredeq  14742  prmdvdsexpr  14748  nnnn0modprm0  14836  pcexp  14888  prmpwdvds  14927  ramcl  15066  cshwshashlem3  15146  cshwrepswhash1  15151  elrestr  15405  xpscfv  15546  mreintcl  15579  mremre  15588  mrieqv2d  15623  initoeu2lem1  15987  funcestrcsetclem9  16111  funcsetcestrclem9  16126  prstr  16256  drsdirfi  16261  latnlej  16392  latnlej2  16395  acsdrsel  16491  acsdrscl  16494  mrelatglb  16508  mrelatlub  16510  isnmgm  16570  mndassOLD  16626  grpinvnz  16803  mulgneg2  16863  gsmsymgrfix  17147  f1omvdco2  17167  symggen  17189  odcl2  17294  odhash3  17303  lsmss1  17394  lsmss2  17396  efgred  17476  efgcpbl  17484  ablfacrp  17777  ablfac1eu  17784  ablfaclem3  17798  dvdsrmul1  17959  dvdsunit  17969  irredmul  18015  lmodlema  18174  ply1scln0  18961  psgnodpmr  19235  lindsss  19459  lindfmm  19462  dmatelnd  19598  mdetdiaglem  19700  mdet0  19708  mdetunilem7  19720  slesolinv  19782  cramerimplem3  19787  cpmatpmat  19811  m2cpminvid2lem  19855  chfacfscmul0  19959  chfacfpmmul0  19963  riinopn  20015  clsndisj  20168  cnpf2  20343  hausnei2  20446  cmpcov  20481  cmpfii  20501  uncon  20521  t1conperf  20528  nrmr0reg  20841  fbfinnfr  20934  filuni  20978  alexsubALT  21144  tmdgsum  21188  cuspcvg  21394  mopni  21585  isngp4  21703  metdsre  21948  metdsreOLD  21963  iimulcl  22043  phtpc01  22105  clmmulg  22202  cfilucfil4  22367  bcthlem5  22374  bcth  22375  bcth3  22377  itg1le  22750  itg2le  22776  bddmulibl  22875  dvnres  22964  cpnord  22968  dvnfre  22985  deg1ge  23126  dgr1term  23293  aaliou3lem2  23378  sincosq1lem  23531  cxpge0  23707  cxpmul2  23713  logrec  23779  sqfpc  24143  bcmono  24284  pntrmax  24481  qabvexp  24543  ostth2lem2  24551  ax5seglem4  25041  axeuclidlem  25071  edgwlk  25338  usgra2wlkspthlem1  25426  usgra2wlkspthlem2  25427  wwlknimp  25494  wlkiswwlk1  25497  wlkiswwlk2  25504  wwlknext  25531  wwlkextproplem2  25549  wwlkext2clwwlk  25610  erclwwlkeqlen  25619  erclwwlksym  25621  erclwwlktr  25622  erclwwlkneqlen  25631  erclwwlknsym  25633  erclwwlkntr  25634  usg2wotspth  25691  usgfiregdegfi  25718  rusgraprop2  25749  rusgraprop3  25750  rusgranumwlk  25764  4cycl2vnunb  25824  usgn0fidegnn0  25836  grpoasscan1  26046  gxnn0neg  26072  gxnn0suc  26073  gxcl  26074  gxneg  26075  gxcom  26078  gxinv  26079  gxsuc  26081  gxnn0add  26083  gxadd  26084  gxnn0mul  26086  gxmul  26087  gxdi  26105  nvs  26372  nvtri  26380  nmlno0  26517  nmlnoubi  26518  ubth  26596  hlipgt0  26647  ocnel  27032  elspansn2  27301  elspansn3  27306  normcan  27310  pjoml2  27345  lecm  27351  osum  27379  nmbdfnlb  27784  leopmul  27868  hstpyth  27963  cvnbtwn  28020  ssmd1  28045  ssmd2  28046  ssdmd1  28047  ssdmd2  28048  cvmd  28070  cvdmd  28071  superpos  28088  disji2f  28264  disjif  28265  disjif2  28268  padct  28382  ffs2  28388  bcm1n  28446  omndadd  28543  ogrpaddlt  28555  archiabl  28589  slmdlema  28593  eulerpartlemb  29274  sgn3da  29485  cvmsdisj  30065  cvmlift2lem12  30109  br1steqg  30487  br2ndeqg  30488  poseq  30562  nosepon  30627  nodenselem8  30648  nofulllem4  30665  lineintmo  30995  nn0prpwlem  31049  nn0prpw  31050  neibastop2lem  31087  bddiblnc  32076  areacirc  32101  incsequz  32141  mettrifi  32150  ismtybnd  32203  heiborlem1  32207  rngoisocnv  32284  risci  32290  lfl1  32707  lkrlsp2  32740  omlfh3N  32896  cvrnbtwn  32908  cvrnbtwn2  32912  cvrnbtwn4  32916  cvlexch3  32969  cvlexch4N  32970  cvlatexchb1  32971  2llnne2N  33044  atcvrj0  33064  cvrat2  33065  ps-1  33113  3atlem5  33123  islln2a  33153  lplnriaN  33186  lplnribN  33187  llncvrlpln2  33193  lplncvrlvol2  33251  psubatN  33391  pmapglb2N  33407  pmapglb2xN  33408  2llnma1b  33422  paddasslem17  33472  pmod2iN  33485  pmodl42N  33487  hlmod1i  33492  atmod1i1  33493  atmod1i2  33495  llnmod1i2  33496  pclcmpatN  33537  osumcllem8N  33599  pexmidlem3N  33608  pl42lem4N  33618  4atexlem7  33711  ltrnnid  33772  cdlemc4  33831  cdleme32a  34079  cdlemeg46gfre  34170  cdlemf2  34200  cdlemg4c  34250  trlcoat  34361  tendovalco  34403  tendoeq2  34412  cdlemk36  34551  diael  34682  diatrl  34683  dicelval1stN  34827  dicelval2nd  34828  dihlspsnat  34972  dochkr1  35117  lcfrlem9  35189  mapdh8e  35423  hdmapval0  35475  hgmapval0  35534  incssnn0  35624  pell14qrexpcl  35784  pell14qrgap  35792  congadd  35887  acongsym  35897  acongtr  35899  dvdsacongtr  35905  jm2.19lem3  35917  jm2.19lem4  35918  jm2.26lem3  35927  relexpiidm  36367  bi13impia  36914  3impcombi  37267  ioogtlb  37688  iocgtlb  37695  iocleub  37696  icoltub  37703  iooltub  37706  limclner  37829  iccpartigtl  38882  wtgoldbnnsum4prm  39042  bgoldbnnsum3prm  39044  bgoldbtbndlem1  39045  bgoldbtbndlem3  39047  bgoldbtbndlem4  39048  bgoldbtbnd  39049  pfx2  39100  pfxccatpfx2  39116  elpr2elpr  39150  2f1fvneq  39158  elfzelfzlble  39206  subsubelfzo0  39207  usgredg4  39458  nbuhgr2vtx1edgblem  39583  vtxduhgr0e  39703  vtxduhgr0nedg  39715  rusgrpropnb  39788  upgr1wlkwlk  39842  red1wlklem  39867  lfgrwlkprop  39879  2pthnloop  39924  spthonepeq-av  39944  pthdlem2lem  39953  crctcsh1wlkn0lem3  39990  crctcsh1wlkn0lem5  39992  crctcsh1wlkn0lem7  39994  crctcsh1wlkn0  39999  2pthon3v-av  40065  uhgr3cyclex  40096  upgreupthseg  40122  eupth2lem3lem4  40143  eucrctshift  40155  usgra2pthspth  40173  c0snmgmhm  40422  funcringcsetcALTV2lem9  40554  funcringcsetclem9ALTV  40577  lincscmcl  40733  lindslinindimp2lem4  40762  lincresunit2  40779  lincresunit3  40782  elfzolborelfzop1  40824  m1modmmod  40832  rege1logbzge0  40878  fllog2  40887  dignn0ldlem  40921
  Copyright terms: Public domain W3C validator