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

Theorem 3impia 1150
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 424 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1147 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  mopick2  2348  3gencl  2986  mob2  3114  moi  3117  reupick3  3626  disjne  3673  disji2  4199  disji  4200  tz7.2  4566  ordintdif  4630  sofld  5318  funopg  5485  fvun1  5794  fvopab6  5826  fprg  5915  isores3  6055  ovmpt4g  6196  ovmpt2s  6197  ov2gf  6198  suppss2  6300  ofrval  6315  poxp  6458  sorpssuni  6531  sorpssint  6532  smoel  6622  smoord  6627  smogt  6629  oaass  6804  oewordi  6834  oeoalem  6839  oeoelem  6841  nnawordi  6864  nnaass  6865  qsel  6983  xpdom3  7206  onsdominel  7256  mapdom3  7279  fisseneq  7320  cantnflem1  7645  cfslbn  8147  cfsmolem  8150  cfcoflem  8152  infpssrlem4  8186  fin23lem7  8196  fin23lem25  8204  isf34lem7  8259  hsmexlem2  8307  axcc3  8318  axdc4lem  8335  tskss  8633  gruss  8671  gruurn  8673  gruiun  8674  gruel  8678  gruen  8687  grudomon  8692  grothac  8705  axpre-sup  9044  axsup  9151  letrp1  9852  p1le  9853  lemul1a  9864  zextle  10343  zextlt  10344  btwnnz  10346  gtndiv  10347  uzind2  10362  fzind  10368  eluzsub  10515  zsupss  10565  xrltne  10753  qbtwnre  10785  qbtwnxr  10786  xlemul1a  10867  iccleub  10967  iccsplit  11029  ceile  11235  modadd1  11278  modmul1  11279  modirr  11286  expcl2lem  11393  expclzlem  11405  expnegz  11414  leexp2r  11437  bcval4  11598  bccmpl  11600  hashbnd  11624  ccatval2  11746  absexpz  12110  climbdd  12465  iseraltlem2  12476  znnenlem  12811  dvdsle  12895  divalgb  12924  ndvdssub  12927  dvdsgcd  13043  rplpwr  13056  qredeq  13106  prmdvdsexpr  13116  pcexp  13233  prmpwdvds  13272  ramcl  13397  elrestr  13656  xpscfv  13787  mreintcl  13820  mremre  13829  mrieqv2d  13864  prstr  14390  drsdirfi  14395  joinle  14450  meetle  14457  latnlej  14497  latnlej2  14500  clatglble  14552  acsdrsel  14593  acsdrscl  14596  mrelatglb  14610  mrelatlub  14612  grpinvnz  14862  mulgneg2  14917  odcl2  15201  odhash3  15210  lsmss1  15298  lsmss2  15300  efgred  15380  efgcpbl  15388  ablfacrp  15624  ablfac1eu  15631  ablfaclem3  15645  dvdsrmul1  15758  dvdsunit  15768  irredmul  15814  lmodlema  15955  ply1scln0  16682  riinopn  16981  clsndisj  17139  cnpf2  17314  hausnei2  17417  cmpcov  17452  cmpfii  17472  bwth  17473  uncon  17492  t1conperf  17499  nrmr0reg  17781  fbfinnfr  17873  filuni  17917  alexsubALT  18082  tmdgsum  18125  cuspcvg  18331  mopni  18522  isngp4  18658  metdsre  18883  iimulcl  18962  phtpc01  19021  clmmulg  19118  cfilucfil4OLD  19273  cfilucfil4  19274  bcthlem5  19281  bcth  19282  bcth3  19284  itg1le  19605  itg2le  19631  bddmulibl  19730  dvnres  19817  cpnord  19821  dvnfre  19838  deg1ge  20021  dgr1term  20178  aaliou3lem2  20260  sincosq1lem  20405  cxpge0  20574  cxpmul2  20580  logrec  20661  sqfpc  20920  bcmono  21061  pntrmax  21258  qabvexp  21320  ostth2lem2  21328  grpoasscan1  21825  gxnn0neg  21851  gxnn0suc  21852  gxcl  21853  gxneg  21854  gxcom  21857  gxinv  21858  gxsuc  21860  gxnn0add  21862  gxadd  21863  gxnn0mul  21865  gxmul  21866  gxdi  21884  nvs  22151  nvtri  22159  nmlno0  22296  nmlnoubi  22297  ubth  22375  hlipgt0  22416  ocnel  22800  elspansn2  23069  elspansn3  23074  normcan  23078  pjoml2  23113  lecm  23119  osum  23147  nmbdfnlb  23553  leopmul  23637  hstpyth  23732  cvnbtwn  23789  ssmd1  23814  ssmd2  23815  ssdmd1  23816  ssdmd2  23817  cvmd  23839  cvdmd  23840  superpos  23857  disji2f  24019  disjif  24020  disjif2  24023  bcm1n  24151  ofldaddlt  24241  cvmsdisj  24957  cvmlift2lem12  25001  binomfallfac  25357  poseq  25528  nodenselem8  25643  nofulllem4  25660  ax5seglem4  25871  axeuclidlem  25901  lineintmo  26091  bddiblnc  26275  areacirc  26297  nn0prpwlem  26325  nn0prpw  26326  neibastop2lem  26389  incsequz  26452  mettrifi  26463  ismtybnd  26516  heiborlem1  26520  rngoisocnv  26597  risci  26603  incssnn0  26765  pell14qrexpcl  26930  pell14qrgap  26938  congadd  27031  acongsym  27041  acongtr  27043  dvdsacongtr  27049  jm2.19lem3  27062  jm2.19lem4  27063  jm2.26lem3  27072  lindsss  27271  lindfmm  27274  f1omvdco2  27368  symggen  27388  2f1fvneq  28077  uzletr  28103  elfz0fzfz0  28114  fzonmapblen  28134  subsubelfzo0  28135  fzofzim  28136  el2fzo  28138  swrdccatin1  28205  2cshw2lem1  28252  2cshw2lem2  28253  cshwssizelem4  28284  usgra2pthspth  28305  usgra2wlkspthlem1  28306  usgra2wlkspthlem2  28307  usg2wotspth  28351  usgfiregdegfi  28361  4cycl2vnunb  28407  bi13impia  28571  3impcombi  28929  lfl1  29868  lkrlsp2  29901  omlfh3N  30057  cvrnbtwn  30069  cvrnbtwn2  30073  cvrnbtwn4  30077  cvlexch3  30130  cvlexch4N  30131  cvlatexchb1  30132  2llnne2N  30205  atcvrj0  30225  cvrat2  30226  ps-1  30274  3atlem5  30284  islln2a  30314  lplnriaN  30347  lplnribN  30348  llncvrlpln2  30354  lplncvrlvol2  30412  psubatN  30552  pmapglb2N  30568  pmapglb2xN  30569  2llnma1b  30583  paddasslem17  30633  pmod2iN  30646  pmodl42N  30648  hlmod1i  30653  atmod1i1  30654  atmod1i2  30656  llnmod1i2  30657  pclcmpatN  30698  osumcllem8N  30760  pexmidlem3N  30769  pl42lem4N  30779  4atexlem7  30872  ltrnnid  30933  cdlemc4  30991  cdleme32a  31238  cdlemeg46gfre  31329  cdlemf2  31359  cdlemg4c  31409  trlcoat  31520  tendovalco  31562  tendoeq2  31571  cdlemk36  31710  diael  31841  diatrl  31842  dicelval1stN  31986  dicelval2nd  31987  dihlspsnat  32131  dochkr1  32276  lcfrlem9  32348  mapdh8e  32582  hdmapval0  32634  hgmapval0  32693
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator