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

Theorem simpll1 994
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 958 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
21adantr 451 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ordiso2  7246  hartogslem1  7273  wemappo  7280  acndom  7694  fin1a2lem12  8053  fin1a2lem13  8054  prlem934  8673  ifle  10540  rpexp  12815  qexpz  12965  ramval  13071  0ram  13083  ramz2  13087  mrelatglb  14303  odbezout  14887  lsmcl  15852  lbsextlem3  15929  psropprmul  16332  coe1mul2  16362  cnconst2  17027  ordthauslem  17127  clscon  17172  restnlly  17224  ptpjopn  17322  trfg  17602  rnelfmlem  17663  isfcf  17745  fcfnei  17746  cnpfcf  17752  blss  17988  metcnp  18103  xrsxmet  18331  metdsge  18369  metdseq0  18374  addcnlem  18384  xrhmeo  18460  nmhmcn  18617  caucfil  18725  limcfval  19238  fta1b  19571  lgsmod  20576  lgsdir  20585  lgsne0  20588  pjhthmo  21897  difioo  23290  xrge0adddir  23347  probun  23637  axpasch  24641  axcontlem2  24665  trisegint  24723  btwnconn1lem13  24794  brsegle2  24804  linethru  24848  icccon2  25803  imonclem  25916  ismonc  25917  idmon  25920  isepic  25927  comppfsc  26410  diophrw  26941  lzunuz  26950  qirropth  27096  jm2.19  27189  jm2.27  27204  lmhmfgsplit  27287  uvcresum  27345  frlmsslsp  27351  islindf4  27411  hbtlem5  27435  rfcnnnub  27810  stoweidlem20  27872  stoweidlem61  27913  hlrelat  30213  intnatN  30218  lnnat  30238  3dim0  30268  3dim1  30278  3dim2  30279  atcvrlln  30331  llnexatN  30332  2at0mat0  30336  llncvrlpln  30369  lplnexllnN  30375  lplncvrlvol  30427  lncvrelatN  30592  lncmp  30594  elpaddn0  30611  paddasslem5  30635  pmapjoin  30663  pmapjat1  30664  pclclN  30702  osumclN  30778  lhprelat3N  30851  trlval4  30999  cdlemd5  31013  cdleme32fvcl  31251  cdleme42keg  31297  cdlemg1a  31381  cdlemg1cN  31398  cdlemg39  31527  ltrncom  31549  cdlemk34  31721  dihord2pre  32037  dihopelvalcpre  32060  dihmeetALTN  32139  dihlspsnssN  32144  dihlspsnat  32145
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