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  7230  hartogslem1  7257  wemappo  7264  acndom  7678  fin1a2lem12  8037  fin1a2lem13  8038  prlem934  8657  ifle  10524  rpexp  12799  qexpz  12949  ramval  13055  0ram  13067  ramz2  13071  mrelatglb  14287  odbezout  14871  lsmcl  15836  lbsextlem3  15913  psropprmul  16316  coe1mul2  16346  cnconst2  17011  ordthauslem  17111  clscon  17156  restnlly  17208  ptpjopn  17306  trfg  17586  rnelfmlem  17647  isfcf  17729  fcfnei  17730  cnpfcf  17736  blss  17972  metcnp  18087  xrsxmet  18315  metdsge  18353  metdseq0  18358  addcnlem  18368  xrhmeo  18444  nmhmcn  18601  caucfil  18709  limcfval  19222  fta1b  19555  lgsmod  20560  lgsdir  20569  lgsne0  20572  pjhthmo  21881  difioo  23275  xrge0adddir  23332  probun  23622  axpasch  24569  axcontlem2  24593  trisegint  24651  btwnconn1lem13  24722  brsegle2  24732  linethru  24776  icccon2  25700  imonclem  25813  ismonc  25814  idmon  25817  isepic  25824  comppfsc  26307  diophrw  26838  lzunuz  26847  qirropth  26993  jm2.19  27086  jm2.27  27101  lmhmfgsplit  27184  uvcresum  27242  frlmsslsp  27248  islindf4  27308  hbtlem5  27332  rfcnnnub  27707  stoweidlem20  27769  stoweidlem61  27810  hlrelat  29591  intnatN  29596  lnnat  29616  3dim0  29646  3dim1  29656  3dim2  29657  atcvrlln  29709  llnexatN  29710  2at0mat0  29714  llncvrlpln  29747  lplnexllnN  29753  lplncvrlvol  29805  lncvrelatN  29970  lncmp  29972  elpaddn0  29989  paddasslem5  30013  pmapjoin  30041  pmapjat1  30042  pclclN  30080  osumclN  30156  lhprelat3N  30229  trlval4  30377  cdlemd5  30391  cdleme32fvcl  30629  cdleme42keg  30675  cdlemg1a  30759  cdlemg1cN  30776  cdlemg39  30905  ltrncom  30927  cdlemk34  31099  dihord2pre  31415  dihopelvalcpre  31438  dihmeetALTN  31517  dihlspsnssN  31522  dihlspsnat  31523
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