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

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

Proof of Theorem simpl2r
StepHypRef Expression
1 simp2r 982 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
21adantr 451 1  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta )  ->  ps )
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  xmulasslem3  10606  pockthg  12953  efgred  15057  lspfixed  15881  uncon  17155  llyrest  17211  basqtop  17402  tmdgsum  17778  tsmsxp  17837  mulcxp  20032  cxple2  20044  cvmlift2lem10  23843  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  outsideofeu  24754  iccss3  25134  cmprltr  25410  islimrs4  25582  idmon  25817  clscnc  26010  isconcl5ab  26102  mzpcong  27059  jm2.25lem1  27091  jm2.26  27095  idomsubgmo  27514  eqlkr  29289  eqlkr2  29290  lkrlsp  29292  atbtwn  29635  3dimlem3OLDN  29651  3dim3  29658  3atlem7  29678  4atlem0a  29782  4atlem3a  29786  4atlem11  29798  lneq2at  29967  lnatexN  29968  paddasslem6  30014  llnexchb2  30058  lhpexle2lem  30198  lhpexle3  30201  lhp2at0nle  30224  lhpat3  30235  trlnid  30368  ltrneq3  30397  cdleme17b  30476  cdleme27cl  30555  cdlemefrs29bpre0  30585  cdlemefrs29clN  30588  cdlemefrs32fva  30589  cdlemefs32sn1aw  30603  cdleme32le  30636  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  tendoex  31164  cdlemm10N  31308  dihord2pre  31415  dihord4  31448  dihord5b  31449  dihglbcpreN  31490  dihmeetlem13N  31509  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