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  5840  omopth2  6598  fin23lem11  7959  xmulasslem3  10622  pockthg  12969  efgred  15073  lspfixed  15897  uncon  17171  llyrest  17227  basqtop  17418  tmdgsum  17794  tsmsxp  17853  mulcxp  20048  cxple2  20060  cvmlift2lem10  23858  br4  24186  ax5seglem1  24628  ax5seglem2  24629  axpasch  24641  axcontlem4  24667  cgrcomim  24684  btwnintr  24714  btwnouttr2  24717  btwndiff  24722  btwnconn1lem14  24795  btwnconn3  24798  segcon2  24800  brsegle  24803  brsegle2  24804  segleantisym  24810  outsideofeu  24826  iccss3  25237  cmprltr  25513  islimrs4  25685  idmon  25920  clscnc  26113  isconcl5ab  26205  mzpcong  27162  jm2.25lem1  27194  jm2.26  27198  idomsubgmo  27617  eqlkr  29911  eqlkr2  29912  lkrlsp  29914  atbtwn  30257  3dimlem3OLDN  30273  3dim3  30280  3atlem7  30300  4atlem0a  30404  4atlem3a  30408  4atlem11  30420  lneq2at  30589  lnatexN  30590  paddasslem6  30636  llnexchb2  30680  lhpexle2lem  30820  lhpexle3  30823  lhp2at0nle  30846  lhpat3  30857  trlnid  30990  ltrneq3  31019  cdleme17b  31098  cdleme27cl  31177  cdlemefrs29bpre0  31207  cdlemefrs29clN  31210  cdlemefrs32fva  31211  cdlemefs32sn1aw  31225  cdleme32le  31258  ltrniotavalbN  31395  cdlemg6  31434  cdlemg7N  31437  cdlemg11b  31453  cdlemg15a  31466  cdlemg15  31467  cdlemg39  31527  trlcone  31539  cdlemg42  31540  tendoconid  31640  tendotr  31641  cdlemk39u  31779  cdlemk19u  31781  tendoex  31786  cdlemm10N  31930  dihord2pre  32037  dihord4  32070  dihord5b  32071  dihglbcpreN  32112  dihmeetlem13N  32131  dih1dimatlem0  32140
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