MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpl1l 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  4778  soisores  5986  omopth2  6763  ramub1lem1  13321  cntzsubr  15827  lbspss  16081  neiptopnei  17119  ptbasin  17530  basqtop  17664  tmdgsum  18046  ustuqtop1  18192  cxplea  20454  cxple2  20455  cvmlift2lem10  24778  5segofs  25654  jm2.25lem1  26760  jm2.26  26764  stoweidlem34  27451  2llnjaN  29680  lvolnle3at  29696  paddasslem12  29945  paddasslem13  29946  atmod1i1m  29972  lhp2lt  30115  lhpexle2lem  30123  lhpmcvr3  30139  lhpat3  30160  ltrneq2  30262  trlnle  30300  trlval3  30301  trlval4  30302  cdleme0moN  30339  cdleme17b  30401  cdlemefrs29pre00  30509  cdlemefr27cl  30517  cdleme42ke  30599  cdleme42mgN  30602  cdleme46f2g2  30607  cdleme46f2g1  30608  cdleme50eq  30655  cdleme50trn3  30667  trlord  30683  cdlemg6c  30734  cdlemg11b  30756  cdlemg18a  30792  cdlemg42  30843  cdlemg46  30849  trljco  30854  tendococl  30886  cdlemj3  30937  tendotr  30944  cdlemk35s-id  31052  cdlemk39s-id  31054  cdlemk53b  31070  cdlemk53  31071  cdlemk35u  31078  tendoex  31089  cdlemm10N  31233  dihopelvalcpre  31363  dihord6apre  31371  dihord5b  31374  dihglblem5apreN  31406  dihglblem2N  31409  dihmeetlem4preN  31421  dihmeetlem6  31424  dihmeetlem10N  31431  dihmeetlem11N  31432  dihmeetlem16N  31437  dihmeetlem17N  31438  dihmeetlem18N  31439  dihmeetlem19N  31440  dihmeetALTN  31442  dihlspsnat  31448  dvh3dim2  31563  dvh3dim3N  31564
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