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

Theorem 3impia 1148
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 423 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1145 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  mopick2  2223  3gencl  2831  mob2  2958  moi  2961  reupick3  3466  disjne  3513  disji2  4026  disji  4027  tz7.2  4393  ordintdif  4457  sofld  5137  funopg  5302  fvun1  5606  fvopab6  5637  isores3  5848  ovmpt4g  5986  ovmpt2s  5987  ov2gf  5988  suppss2  6089  ofrval  6104  poxp  6243  sorpssuni  6302  sorpssint  6303  smoel  6393  smoord  6398  smogt  6400  oaass  6575  oewordi  6605  oeoalem  6610  oeoelem  6612  nnawordi  6635  nnaass  6636  qsel  6754  xpdom3  6976  onsdominel  7026  mapdom3  7049  fisseneq  7090  cantnflem1  7407  cfslbn  7909  cfsmolem  7912  cfcoflem  7914  infpssrlem4  7948  fin23lem7  7958  fin23lem25  7966  isf34lem7  8021  hsmexlem2  8069  axcc3  8080  axdc4lem  8097  tskss  8396  gruss  8434  gruurn  8436  gruiun  8437  gruel  8441  gruen  8450  grudomon  8455  grothac  8468  axpre-sup  8807  axsup  8914  letrp1  9614  p1le  9615  lemul1a  9626  zextle  10101  zextlt  10102  btwnnz  10104  gtndiv  10105  uzind2  10120  fzind  10126  eluzsub  10273  zsupss  10323  xrltne  10510  qbtwnre  10542  qbtwnxr  10543  xlemul1a  10624  iccleub  10723  iccsplit  10784  ceile  10974  modadd1  11017  modmul1  11018  modirr  11025  expcl2lem  11131  expclzlem  11143  expnegz  11152  leexp2r  11175  bcval4  11336  bccmpl  11338  hashbnd  11359  ccatval2  11448  absexpz  11806  abssubne0  11816  iseraltlem2  12171  znnenlem  12506  dvdsle  12590  divalgb  12619  ndvdssub  12622  dvdsgcd  12738  rplpwr  12751  qredeq  12801  prmdvdsexpr  12811  pcexp  12928  prmpwdvds  12967  ramcl  13092  elrestr  13349  xpscfv  13480  mreintcl  13513  mremre  13522  mrieqv2d  13557  prstr  14083  drsdirfi  14088  joinle  14143  meetle  14150  latnlej  14190  latnlej2  14193  clatglble  14245  acsdrsel  14286  acsdrscl  14289  mrelatglb  14303  mrelatlub  14305  grpinvnz  14555  mulgneg2  14610  odcl2  14894  odhash3  14903  lsmss1  14991  lsmss2  14993  efgred  15073  efgcpbl  15081  ablfacrp  15317  ablfac1eu  15324  ablfaclem3  15338  dvdsrmul1  15451  dvdsunit  15461  irredmul  15507  lmodlema  15648  lmodvsdi1OLD  15667  ply1scln0  16382  riinopn  16670  clsndisj  16828  cnpf2  16996  hausnei2  17097  cmpcov  17132  cmpfii  17152  uncon  17171  t1conperf  17178  nrmr0reg  17456  fbfinnfr  17552  filuni  17596  alexsubALT  17761  tmdgsum  17794  mopni  18054  isngp4  18149  metdsre  18373  iimulcl  18451  phtpc01  18510  clmmulg  18607  bcthlem5  18766  bcth  18767  bcth3  18769  itg1le  19084  itg2le  19110  bddmulibl  19209  dvnres  19296  cpnord  19300  dvnfre  19317  deg1ge  19500  dgr1term  19657  aaliou3lem2  19739  sincosq1lem  19881  cxpge0  20046  cxpmul2  20052  logrec  20133  sqfpc  20391  bcmono  20532  pntrmax  20729  qabvexp  20791  ostth2lem2  20799  grpoasscan1  20920  gxnn0neg  20946  gxnn0suc  20947  gxcl  20948  gxneg  20949  gxcom  20952  gxinv  20953  gxsuc  20955  gxnn0add  20957  gxadd  20958  gxnn0mul  20960  gxmul  20961  gxdi  20979  nvs  21244  nvtri  21252  nmlno0  21389  nmlnoubi  21390  ubth  21468  hlipgt0  21509  ocnel  21893  elspansn2  22162  elspansn3  22167  normcan  22171  pjoml2  22206  lecm  22212  osum  22240  nmbdfnlb  22646  leopmul  22730  hstpyth  22825  cvnbtwn  22882  ssmd1  22907  ssmd2  22908  ssdmd1  22909  ssdmd2  22910  cvmd  22932  cvdmd  22933  superpos  22950  bcm1n  23048  ballotlemfc0  23067  ballotlemfcc  23068  disji2f  23369  disjif  23370  disjif2  23373  cvmsdisj  23816  cvmlift2lem12  23860  poseq  24324  nodenselem8  24413  nofulllem4  24430  ax5seglem4  24632  axeuclidlem  24662  lineintmo  24852  itg2addnc  25005  bddiblnc  25021  areacirc  25034  ab2rexex2g  25235  fprg  25236  iccleub2  25238  iccleub3  25239  jop  25287  mop  25288  labs1  25291  labs2  25293  valcurfn  25306  mgmlion  25440  imtr  25501  intfmu2  25622  islimrs3  25684  bwt2  25695  dmse1  25706  mslb1  25710  2wsms  25711  lvsovso  25729  cmpassoh  25904  cmpmon  25918  icmpmon  25919  nn0prpwlem  26341  nn0prpw  26342  neibastop2lem  26412  incsequz  26561  mettrifi  26576  ismtybnd  26634  heiborlem1  26638  rngoisocnv  26715  risci  26721  incssnn0  26889  pell14qrexpcl  27055  pell14qrgap  27063  congadd  27156  acongsym  27166  acongtr  27168  dvdsacongtr  27174  jm2.19lem3  27187  jm2.19lem4  27188  jm2.26lem3  27197  lindsss  27397  lindfmm  27400  f1omvdco2  27494  symggen  27514  stoweidlem34  27886  4cycl2vnunb  28439  bi13impia  28552  bi123impia  28553  3impcombi  28906  lfl1  29882  lkrlsp2  29915  omlfh3N  30071  cvrnbtwn  30083  cvrnbtwn2  30087  cvrnbtwn4  30091  cvlexch3  30144  cvlexch4N  30145  cvlatexchb1  30146  2llnne2N  30219  atcvrj0  30239  cvrat2  30240  ps-1  30288  3atlem5  30298  islln2a  30328  lplnriaN  30361  lplnribN  30362  llncvrlpln2  30368  lplncvrlvol2  30426  psubatN  30566  pmapglb2N  30582  pmapglb2xN  30583  2llnma1b  30597  paddasslem17  30647  pmod2iN  30660  pmodl42N  30662  hlmod1i  30667  atmod1i1  30668  atmod1i2  30670  llnmod1i2  30671  pclcmpatN  30712  osumcllem8N  30774  pexmidlem3N  30783  pl42lem4N  30793  4atexlem7  30886  ltrnnid  30947  cdlemc4  31005  cdleme32a  31252  cdlemeg46gfre  31343  cdlemf2  31373  cdlemg4c  31423  trlcoat  31534  tendovalco  31576  tendoeq2  31585  cdlemk36  31724  diael  31855  diatrl  31856  dicelval1stN  32000  dicelval2nd  32001  dihlspsnat  32145  dochkr1  32290  lcfrlem9  32362  mapdh8e  32596  hdmapval0  32648  hgmapval0  32707
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator