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

Theorem simpl2r 1012
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 985 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
21adantr 453 1  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  soisores  6049  omopth2  6829  fin23lem11  8199  xmulasslem3  10867  pockthg  13276  efgred  15382  lspfixed  16202  uncon  17494  llyrest  17550  basqtop  17745  tmdgsum  18127  tsmsxp  18186  ucncn  18317  mulcxp  20578  cxple2  20590  cvmlift2lem10  25001  ntrivcvgmul  25232  br4  25383  ax5seglem1  25869  ax5seglem2  25870  axpasch  25882  axcontlem4  25908  cgrcomim  25925  btwnintr  25955  btwnouttr2  25958  btwndiff  25963  btwnconn1lem14  26036  btwnconn3  26039  segcon2  26041  brsegle  26044  brsegle2  26045  segleantisym  26051  outsideofeu  26067  mzpcong  27039  jm2.25lem1  27071  jm2.26  27075  idomsubgmo  27493  wlklniswwlkn1  28369  eqlkr  29959  eqlkr2  29960  lkrlsp  29962  atbtwn  30305  3dimlem3OLDN  30321  3dim3  30328  3atlem7  30348  4atlem0a  30452  4atlem3a  30456  4atlem11  30468  lneq2at  30637  lnatexN  30638  paddasslem6  30684  llnexchb2  30728  lhpexle2lem  30868  lhpexle3  30871  lhp2at0nle  30894  lhpat3  30905  trlnid  31038  ltrneq3  31067  cdleme17b  31146  cdleme27cl  31225  cdlemefrs29bpre0  31255  cdlemefrs29clN  31258  cdlemefrs32fva  31259  cdlemefs32sn1aw  31273  cdleme32le  31306  ltrniotavalbN  31443  cdlemg6  31482  cdlemg7N  31485  cdlemg11b  31501  cdlemg15a  31514  cdlemg15  31515  cdlemg39  31575  trlcone  31587  cdlemg42  31588  tendoconid  31688  tendotr  31689  cdlemk39u  31827  cdlemk19u  31829  tendoex  31834  cdlemm10N  31978  dihord2pre  32085  dihord4  32118  dihord5b  32119  dihglbcpreN  32160  dihmeetlem13N  32179  dih1dimatlem0  32188
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator