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

Theorem simpl1l 1008
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 981 . 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:  tfisi  4831  soisores  6040  omopth2  6820  ramub1lem1  13387  cntzsubr  15893  lbspss  16147  neiptopnei  17189  ptbasin  17602  basqtop  17736  tmdgsum  18118  ustuqtop1  18264  cxplea  20580  cxple2  20581  isarchi2  24248  cvmlift2lem10  24992  5segofs  25933  jm2.25lem1  27061  jm2.26  27065  stoweidlem34  27751  2llnjaN  30301  lvolnle3at  30317  paddasslem12  30566  paddasslem13  30567  atmod1i1m  30593  lhp2lt  30736  lhpexle2lem  30744  lhpmcvr3  30760  lhpat3  30781  ltrneq2  30883  trlnle  30921  trlval3  30922  trlval4  30923  cdleme0moN  30960  cdleme17b  31022  cdlemefrs29pre00  31130  cdlemefr27cl  31138  cdleme42ke  31220  cdleme42mgN  31223  cdleme46f2g2  31228  cdleme46f2g1  31229  cdleme50eq  31276  cdleme50trn3  31288  trlord  31304  cdlemg6c  31355  cdlemg11b  31377  cdlemg18a  31413  cdlemg42  31464  cdlemg46  31470  trljco  31475  tendococl  31507  cdlemj3  31558  tendotr  31565  cdlemk35s-id  31673  cdlemk39s-id  31675  cdlemk53b  31691  cdlemk53  31692  cdlemk35u  31699  tendoex  31710  cdlemm10N  31854  dihopelvalcpre  31984  dihord6apre  31992  dihord5b  31995  dihglblem5apreN  32027  dihglblem2N  32030  dihmeetlem4preN  32042  dihmeetlem6  32045  dihmeetlem10N  32052  dihmeetlem11N  32053  dihmeetlem16N  32058  dihmeetlem17N  32059  dihmeetlem18N  32060  dihmeetlem19N  32061  dihmeetALTN  32063  dihlspsnat  32069  dvh3dim2  32184  dvh3dim3N  32185
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