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

Theorem simpll1 1045
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpll1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ph )

Proof of Theorem simpll1
StepHypRef Expression
1 simpl1 1009 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
21adantr 467 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  f1prex  6196  ordiso2  8038  hartogslem1  8065  wemappo  8072  wemapso2lem  8075  acndom  8488  fin1a2lem12  8847  fin1a2lem13  8848  prlem934  9464  ifle  11496  lcmfunsnlem2lem1  14608  rpexp  14669  qexpz  14843  ramval  14957  ramvalOLD  14958  0ram  14975  ramz2  14979  initoeu2lem2  15907  mrelatglb  16427  odbezout  17206  lsmcl  18303  lbsextlem3  18380  psropprmul  18828  coe1mul2  18859  coe1fzgsumdlem  18892  evl1gsumdlem  18941  frlmsslsp  19350  islindf4  19392  scmate  19531  mdetunilem7  19639  mdetmul  19644  cramerlem2  19709  m2pmfzgsumcl  19768  decpmatmul  19792  pmatcollpw3lem  19803  chpdmatlem2  19859  cpmadugsumlemB  19894  cpmadugsumlemC  19895  cpmadugsumlemF  19896  chcoeffeqlem  19905  cnconst2  20295  ordthauslem  20395  clscon  20441  restnlly  20493  comppfsc  20543  ptpjopn  20623  trfg  20902  rnelfmlem  20963  isfcf  21045  fcfnei  21046  cnpfcf  21052  utop2nei  21261  neipcfilu  21307  blssps  21435  blss  21436  metcnp  21552  xrsxmet  21823  metdsge  21862  metdseq0  21867  metdsgeOLD  21877  metdseq0OLD  21882  addcnlem  21892  xrhmeo  21970  nmhmcn  22130  caucfil  22249  limcfval  22823  fta1b  23116  lgsmod  24245  lgsdir  24254  lgsne0  24257  axpasch  24967  axcontlem2  24991  clwwlknwwlkncl  25524  clwlkf1clwwlk  25574  pjhthmo  26951  difioo  28368  xrge0adddir  28460  archiabl  28520  rhmdvdsr  28587  probun  29258  trisegint  30798  btwnconn1lem13  30869  brsegle2  30879  linethru  30923  hlrelat  32934  intnatN  32939  lnnat  32959  3dim0  32989  3dim1  32999  3dim2  33000  atcvrlln  33052  llnexatN  33053  2at0mat0  33057  llncvrlpln  33090  lplnexllnN  33096  lplncvrlvol  33148  lncvrelatN  33313  lncmp  33315  elpaddn0  33332  paddasslem5  33356  pmapjoin  33384  pmapjat1  33385  pclclN  33423  osumclN  33499  lhprelat3N  33572  trlval4  33721  cdlemd5  33735  cdleme32fvcl  33974  cdleme42keg  34020  cdlemg1a  34104  cdlemg1cN  34121  cdlemg39  34250  ltrncom  34272  cdlemk34  34444  dihord2pre  34760  dihopelvalcpre  34783  dihmeetALTN  34862  dihlspsnssN  34867  dihlspsnat  34868  diophrw  35568  lzunuz  35577  qirropth  35724  jm2.19  35816  jm2.27  35831  lmhmfgsplit  35912  hbtlem5  35955  iunrelexpuztr  36219  rfcnnnub  37266  3adantll2  37273  3adantll3  37274  ioondisj2  37468  ioondisj1  37469  iccintsng  37503  icccncfext  37633  stoweidlem20  37748  stoweidlem61  37790  rmsupp0  39547  rmsuppss  39549  ply1mulgsum  39576
  Copyright terms: Public domain W3C validator