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

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

Proof of Theorem simpl2l
StepHypRef Expression
1 simp2l 981 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
21adantr 451 1  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  soisores  5824  omopth2  6582  fin23lem11  7943  xaddass  10569  pockthg  12953  efgred  15057  uncon  17155  basqtop  17402  cxple2  20044  cxple2a  20046  cvmlift2lem10  23843  dedekind  24082  br4  24115  ax5seglem1  24556  ax5seglem2  24557  axpasch  24569  axcontlem4  24595  cgrcomim  24612  btwnintr  24642  btwnouttr2  24645  btwndiff  24650  btwnconn1lem14  24723  btwnconn3  24726  segcon2  24728  brsegle  24731  brsegle2  24732  segleantisym  24738  seglelin  24739  outsideofeu  24754  iccss3  25134  cmprltr  25410  islimrs4  25582  idmon  25817  isconcl5ab  26102  qirropth  26993  mzpcong  27059  jm2.25lem1  27091  jm2.26  27095  idomsubgmo  27514  eqlkr  29289  eqlkr2  29290  lkrlsp  29292  atbtwn  29635  athgt  29645  3dimlem3  29650  3dimlem3OLDN  29651  3dim3  29658  3atlem7  29678  4atlem0a  29782  4atlem3a  29786  4atlem11  29798  lneq2at  29967  lnatexN  29968  cdlemb  29983  paddasslem6  30014  llnexchb2  30058  lhp2lt  30190  lhpexle2lem  30198  lhpexle3  30201  lhpmcvr3  30214  lhpat3  30235  ltrnnidn  30363  ltrneq3  30397  cdleme17b  30476  cdleme25a  30542  cdleme25dN  30545  cdleme27cl  30555  cdlemefrs29bpre0  30585  cdlemefs32sn1aw  30603  cdleme32le  30636  cdleme46f2g2  30682  cdleme46f2g1  30683  cdleme50trn3  30742  trlord  30758  ltrniotavalbN  30773  cdlemg6  30812  cdlemg7N  30815  cdlemg11b  30831  cdlemg15a  30844  cdlemg15  30845  cdlemg39  30905  trlcone  30917  cdlemg42  30918  tendoconid  31018  tendotr  31019  cdlemk39u  31157  cdlemk19u  31159  cdleml5N  31169  cdlemm10N  31308  dihord11b  31412  dihord2pre  31415  dihvalcqpre  31425  dihopelvalcpre  31438  dihord6apre  31446  dihord4  31448  dihord5b  31449  dihglblem5apreN  31481  dihmeetlem13N  31509  dihmeetlem19N  31515  dih1dimatlem0  31518
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