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

Theorem simpl1l 1039
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 1012 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
21adantr 465 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  soisores  6120  tfisi  6572  omopth2  7126  repswswrd  12533  ramub1lem1  14198  cntzsubr  17012  lbspss  17278  maducoeval2  18571  cramer  18622  neiptopnei  18861  ptbasin  19275  basqtop  19409  tmdgsum  19791  ustuqtop1  19941  cxplea  22267  cxple2  22268  br8d  26086  isarchi2  26340  archiabllem2c  26350  cvmlift2lem10  27338  5segofs  28174  jm2.25lem1  29488  jm2.26  29492  stoweidlem34  29970  usg2wlkeq2  30482  domnmsuppn0  30923  2llnjaN  33519  lvolnle3at  33535  paddasslem12  33784  paddasslem13  33785  atmod1i1m  33811  lhp2lt  33954  lhpexle2lem  33962  lhpmcvr3  33978  lhpat3  33999  ltrneq2  34101  trlnle  34139  trlval3  34140  trlval4  34141  cdleme0moN  34178  cdleme17b  34240  cdlemefrs29pre00  34348  cdlemefr27cl  34356  cdleme42ke  34438  cdleme42mgN  34441  cdleme46f2g2  34446  cdleme46f2g1  34447  cdleme50eq  34494  cdleme50trn3  34506  trlord  34522  cdlemg6c  34573  cdlemg11b  34595  cdlemg18a  34631  cdlemg42  34682  cdlemg46  34688  trljco  34693  tendococl  34725  cdlemj3  34776  tendotr  34783  cdlemk35s-id  34891  cdlemk39s-id  34893  cdlemk53b  34909  cdlemk53  34910  cdlemk35u  34917  tendoex  34928  cdlemm10N  35072  dihopelvalcpre  35202  dihord6apre  35210  dihord5b  35213  dihglblem5apreN  35245  dihglblem2N  35248  dihmeetlem4preN  35260  dihmeetlem6  35263  dihmeetlem10N  35270  dihmeetlem11N  35271  dihmeetlem16N  35276  dihmeetlem17N  35277  dihmeetlem18N  35278  dihmeetlem19N  35279  dihmeetALTN  35281  dihlspsnat  35287  dvh3dim2  35402  dvh3dim3N  35403
  Copyright terms: Public domain W3C validator