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  4665  soisores  5840  omopth2  6598  ramub1lem1  13089  cntzsubr  15593  lbspss  15851  ptbasin  17288  basqtop  17418  tmdgsum  17794  cxplea  20059  cxple2  20060  cvmlift2lem10  23858  5segofs  24701  iccss3  25237  jm2.25lem1  27194  jm2.26  27198  stoweidlem34  27886  2llnjaN  30377  lvolnle3at  30393  paddasslem12  30642  paddasslem13  30643  atmod1i1m  30669  lhp2lt  30812  lhpexle2lem  30820  lhpmcvr3  30836  lhpat3  30857  ltrneq2  30959  trlnle  30997  trlval3  30998  trlval4  30999  cdleme0moN  31036  cdleme17b  31098  cdlemefrs29pre00  31206  cdlemefr27cl  31214  cdleme42ke  31296  cdleme42mgN  31299  cdleme46f2g2  31304  cdleme46f2g1  31305  cdleme50eq  31352  cdleme50trn3  31364  trlord  31380  cdlemg6c  31431  cdlemg11b  31453  cdlemg18a  31489  cdlemg42  31540  cdlemg46  31546  trljco  31551  tendococl  31583  cdlemj3  31634  tendotr  31641  cdlemk35s-id  31749  cdlemk39s-id  31751  cdlemk53b  31767  cdlemk53  31768  cdlemk35u  31775  tendoex  31786  cdlemm10N  31930  dihopelvalcpre  32060  dihord6apre  32068  dihord5b  32071  dihglblem5apreN  32103  dihglblem2N  32106  dihmeetlem4preN  32118  dihmeetlem6  32121  dihmeetlem10N  32128  dihmeetlem11N  32129  dihmeetlem16N  32134  dihmeetlem17N  32135  dihmeetlem18N  32136  dihmeetlem19N  32137  dihmeetALTN  32139  dihlspsnat  32145  dvh3dim2  32260  dvh3dim3N  32261
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