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

Theorem simpll1 996
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 960 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
21adantr 452 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ordiso2  7474  hartogslem1  7501  wemappo  7508  acndom  7922  fin1a2lem12  8281  fin1a2lem13  8282  prlem934  8900  ifle  10773  rpexp  13110  qexpz  13260  ramval  13366  0ram  13378  ramz2  13382  mrelatglb  14600  odbezout  15184  lsmcl  16145  lbsextlem3  16222  psropprmul  16622  coe1mul2  16652  cnconst2  17337  ordthauslem  17437  clscon  17483  restnlly  17535  ptpjopn  17634  trfg  17913  rnelfmlem  17974  isfcf  18056  fcfnei  18057  cnpfcf  18063  utop2nei  18270  neipcfilu  18316  blssps  18444  blss  18445  metcnp  18561  xrsxmet  18830  metdsge  18869  metdseq0  18874  addcnlem  18884  xrhmeo  18961  nmhmcn  19118  caucfil  19226  limcfval  19749  fta1b  20082  lgsmod  21095  lgsdir  21104  lgsne0  21107  pjhthmo  22794  difioo  24135  xrge0adddir  24205  rhmdvdsr  24246  probun  24667  axpasch  25845  axcontlem2  25869  trisegint  25927  btwnconn1lem13  25998  brsegle2  26008  linethru  26052  comppfsc  26341  diophrw  26771  lzunuz  26780  qirropth  26925  jm2.19  27018  jm2.27  27033  lmhmfgsplit  27116  uvcresum  27174  frlmsslsp  27180  islindf4  27240  hbtlem5  27264  rfcnnnub  27638  stoweidlem20  27700  stoweidlem61  27741  hlrelat  30100  intnatN  30105  lnnat  30125  3dim0  30155  3dim1  30165  3dim2  30166  atcvrlln  30218  llnexatN  30219  2at0mat0  30223  llncvrlpln  30256  lplnexllnN  30262  lplncvrlvol  30314  lncvrelatN  30479  lncmp  30481  elpaddn0  30498  paddasslem5  30522  pmapjoin  30550  pmapjat1  30551  pclclN  30589  osumclN  30665  lhprelat3N  30738  trlval4  30886  cdlemd5  30900  cdleme32fvcl  31138  cdleme42keg  31184  cdlemg1a  31268  cdlemg1cN  31285  cdlemg39  31414  ltrncom  31436  cdlemk34  31608  dihord2pre  31924  dihopelvalcpre  31947  dihmeetALTN  32026  dihlspsnssN  32031  dihlspsnat  32032
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator