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  2210  3gencl  2818  mob2  2945  moi  2948  reupick3  3453  disjne  3500  disji2  4010  disji  4011  tz7.2  4377  ordintdif  4441  sofld  5121  funopg  5286  fvun1  5590  fvopab6  5621  isores3  5832  ovmpt4g  5970  ovmpt2s  5971  ov2gf  5972  suppss2  6073  ofrval  6088  poxp  6227  sorpssuni  6286  sorpssint  6287  smoel  6377  smoord  6382  smogt  6384  oaass  6559  oewordi  6589  oeoalem  6594  oeoelem  6596  nnawordi  6619  nnaass  6620  qsel  6738  xpdom3  6960  onsdominel  7010  mapdom3  7033  fisseneq  7074  cantnflem1  7391  cfslbn  7893  cfsmolem  7896  cfcoflem  7898  infpssrlem4  7932  fin23lem7  7942  fin23lem25  7950  isf34lem7  8005  hsmexlem2  8053  axcc3  8064  axdc4lem  8081  tskss  8380  gruss  8418  gruurn  8420  gruiun  8421  gruel  8425  gruen  8434  grudomon  8439  grothac  8452  axpre-sup  8791  axsup  8898  letrp1  9598  p1le  9599  lemul1a  9610  zextle  10085  zextlt  10086  btwnnz  10088  gtndiv  10089  uzind2  10104  fzind  10110  eluzsub  10257  zsupss  10307  xrltne  10494  qbtwnre  10526  qbtwnxr  10527  xlemul1a  10608  iccleub  10707  iccsplit  10768  ceile  10958  modadd1  11001  modmul1  11002  modirr  11009  expcl2lem  11115  expclzlem  11127  expnegz  11136  leexp2r  11159  bcval4  11320  bccmpl  11322  hashbnd  11343  ccatval2  11432  absexpz  11790  abssubne0  11800  iseraltlem2  12155  znnenlem  12490  dvdsle  12574  divalgb  12603  ndvdssub  12606  dvdsgcd  12722  rplpwr  12735  qredeq  12785  prmdvdsexpr  12795  pcexp  12912  prmpwdvds  12951  ramcl  13076  elrestr  13333  xpscfv  13464  mreintcl  13497  mremre  13506  mrieqv2d  13541  prstr  14067  drsdirfi  14072  joinle  14127  meetle  14134  latnlej  14174  latnlej2  14177  clatglble  14229  acsdrsel  14270  acsdrscl  14273  mrelatglb  14287  mrelatlub  14289  grpinvnz  14539  mulgneg2  14594  odcl2  14878  odhash3  14887  lsmss1  14975  lsmss2  14977  efgred  15057  efgcpbl  15065  ablfacrp  15301  ablfac1eu  15308  ablfaclem3  15322  dvdsrmul1  15435  dvdsunit  15445  irredmul  15491  lmodlema  15632  lmodvsdi1OLD  15651  ply1scln0  16366  riinopn  16654  clsndisj  16812  cnpf2  16980  hausnei2  17081  cmpcov  17116  cmpfii  17136  uncon  17155  t1conperf  17162  nrmr0reg  17440  fbfinnfr  17536  filuni  17580  alexsubALT  17745  tmdgsum  17778  mopni  18038  isngp4  18133  metdsre  18357  iimulcl  18435  phtpc01  18494  clmmulg  18591  bcthlem5  18750  bcth  18751  bcth3  18753  itg1le  19068  itg2le  19094  bddmulibl  19193  dvnres  19280  cpnord  19284  dvnfre  19301  deg1ge  19484  dgr1term  19641  aaliou3lem2  19723  sincosq1lem  19865  cxpge0  20030  cxpmul2  20036  logrec  20117  sqfpc  20375  bcmono  20516  pntrmax  20713  qabvexp  20775  ostth2lem2  20783  grpoasscan1  20904  gxnn0neg  20930  gxnn0suc  20931  gxcl  20932  gxneg  20933  gxcom  20936  gxinv  20937  gxsuc  20939  gxnn0add  20941  gxadd  20942  gxnn0mul  20944  gxmul  20945  gxdi  20963  nvs  21228  nvtri  21236  nmlno0  21373  nmlnoubi  21374  ubth  21452  hlipgt0  21493  ocnel  21877  elspansn2  22146  elspansn3  22151  normcan  22155  pjoml2  22190  lecm  22196  osum  22224  nmbdfnlb  22630  leopmul  22714  hstpyth  22809  cvnbtwn  22866  ssmd1  22891  ssmd2  22892  ssdmd1  22893  ssdmd2  22894  cvmd  22916  cvdmd  22917  superpos  22934  bcm1n  23032  ballotlemfc0  23051  ballotlemfcc  23052  disji2f  23354  disjif  23355  disjif2  23358  cvmsdisj  23801  cvmlift2lem12  23845  poseq  24253  nodenselem8  24342  nofulllem4  24359  ax5seglem4  24560  axeuclidlem  24590  lineintmo  24780  areacirc  24931  ab2rexex2g  25132  fprg  25133  iccleub2  25135  iccleub3  25136  jop  25184  mop  25185  labs1  25188  labs2  25190  valcurfn  25203  mgmlion  25337  imtr  25398  intfmu2  25519  islimrs3  25581  bwt2  25592  dmse1  25603  mslb1  25607  2wsms  25608  lvsovso  25626  cmpassoh  25801  cmpmon  25815  icmpmon  25816  nn0prpwlem  26238  nn0prpw  26239  neibastop2lem  26309  incsequz  26458  mettrifi  26473  ismtybnd  26531  heiborlem1  26535  rngoisocnv  26612  risci  26618  incssnn0  26786  pell14qrexpcl  26952  pell14qrgap  26960  congadd  27053  acongsym  27063  acongtr  27065  dvdsacongtr  27071  jm2.19lem3  27084  jm2.19lem4  27085  jm2.26lem3  27094  lindsss  27294  lindfmm  27297  f1omvdco2  27391  symggen  27411  stoweidlem34  27783  lfl1  29260  lkrlsp2  29293  omlfh3N  29449  cvrnbtwn  29461  cvrnbtwn2  29465  cvrnbtwn4  29469  cvlexch3  29522  cvlexch4N  29523  cvlatexchb1  29524  2llnne2N  29597  atcvrj0  29617  cvrat2  29618  ps-1  29666  3atlem5  29676  islln2a  29706  lplnriaN  29739  lplnribN  29740  llncvrlpln2  29746  lplncvrlvol2  29804  psubatN  29944  pmapglb2N  29960  pmapglb2xN  29961  2llnma1b  29975  paddasslem17  30025  pmod2iN  30038  pmodl42N  30040  hlmod1i  30045  atmod1i1  30046  atmod1i2  30048  llnmod1i2  30049  pclcmpatN  30090  osumcllem8N  30152  pexmidlem3N  30161  pl42lem4N  30171  4atexlem7  30264  ltrnnid  30325  cdlemc4  30383  cdleme32a  30630  cdlemeg46gfre  30721  cdlemf2  30751  cdlemg4c  30801  trlcoat  30912  tendovalco  30954  tendoeq2  30963  cdlemk36  31102  diael  31233  diatrl  31234  dicelval1stN  31378  dicelval2nd  31379  dihlspsnat  31523  dochkr1  31668  lcfrlem9  31740  mapdh8e  31974  hdmapval0  32026  hgmapval0  32085
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