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

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

Proof of Theorem simpl1l
StepHypRef Expression
1 simp1l 979 . 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:  tfisi  4649  soisores  5824  omopth2  6582  ramub1lem1  13073  cntzsubr  15577  lbspss  15835  ptbasin  17272  basqtop  17402  tmdgsum  17778  cxplea  20043  cxple2  20044  cvmlift2lem10  23843  5segofs  24629  iccss3  25134  jm2.25lem1  27091  jm2.26  27095  stoweidlem34  27783  2llnjaN  29755  lvolnle3at  29771  paddasslem12  30020  paddasslem13  30021  atmod1i1m  30047  lhp2lt  30190  lhpexle2lem  30198  lhpmcvr3  30214  lhpat3  30235  ltrneq2  30337  trlnle  30375  trlval3  30376  trlval4  30377  cdleme0moN  30414  cdleme17b  30476  cdlemefrs29pre00  30584  cdlemefr27cl  30592  cdleme42ke  30674  cdleme42mgN  30677  cdleme46f2g2  30682  cdleme46f2g1  30683  cdleme50eq  30730  cdleme50trn3  30742  trlord  30758  cdlemg6c  30809  cdlemg11b  30831  cdlemg18a  30867  cdlemg42  30918  cdlemg46  30924  trljco  30929  tendococl  30961  cdlemj3  31012  tendotr  31019  cdlemk35s-id  31127  cdlemk39s-id  31129  cdlemk53b  31145  cdlemk53  31146  cdlemk35u  31153  tendoex  31164  cdlemm10N  31308  dihopelvalcpre  31438  dihord6apre  31446  dihord5b  31449  dihglblem5apreN  31481  dihglblem2N  31484  dihmeetlem4preN  31496  dihmeetlem6  31499  dihmeetlem10N  31506  dihmeetlem11N  31507  dihmeetlem16N  31512  dihmeetlem17N  31513  dihmeetlem18N  31514  dihmeetlem19N  31515  dihmeetALTN  31517  dihlspsnat  31523  dvh3dim2  31638  dvh3dim3N  31639
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