Theorem simpl2r 1059

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpl2r	|- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta ) -> ps )

Proof of Theorem simpl2r

Step	Hyp	Ref	Expression
1		simp2r 1032	. 2 |- ( ( ch /\ ( ph /\ ps ) /\ th ) -> ps )
2	1	adantr 466	1 |- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  soisores  6229  omopth2  7289  fin23lem11  8747  xmulasslem3  11572  ssfzo12bi  12005  ntrivcvgmul  13943  pockthg  14835  gsmsymgreqlem2  17057  efgred  17383  lspfixed  18336  decpmatmullem  19779  decpmatmul  19780  uncon  20428  llyrest  20484  basqtop  20710  tmdgsum  21094  tsmsxp  21153  ucncn  21284  mulcxp  23614  cxple2  23626  ax5seglem1  24942  ax5seglem2  24943  axpasch  24955  axcontlem4  24981  wlklniswwlkn1  25410  cvmlift2lem10  30028  br4  30390  cgrcomim  30746  btwnintr  30776  btwnouttr2  30779  btwndiff  30784  btwnconn1lem14  30857  btwnconn3  30860  segcon2  30862  brsegle  30865  brsegle2  30866  segleantisym  30872  outsideofeu  30888  eqlkr  32581  eqlkr2  32582  lkrlsp  32584  atbtwn  32927  3dimlem3OLDN  32943  3dim3  32950  3atlem7  32970  4atlem0a  33074  4atlem3a  33078  4atlem11  33090  lneq2at  33259  lnatexN  33260  paddasslem6  33306  llnexchb2  33350  lhpexle2lem  33490  lhpexle3  33493  lhp2at0nle  33516  lhpat3  33527  trlnid  33661  ltrneq3  33690  cdleme17b  33769  cdleme27cl  33849  cdlemefrs29bpre0  33879  cdlemefrs29clN  33882  cdlemefrs32fva  33883  cdlemefs32sn1aw  33897  cdleme32le  33930  ltrniotavalbN  34067  cdlemg6  34106  cdlemg7N  34109  cdlemg11b  34125  cdlemg15a  34138  cdlemg15  34139  cdlemg39  34199  trlcone  34211  cdlemg42  34212  tendoconid  34312  tendotr  34313  cdlemk39u  34451  cdlemk19u  34453  tendoex  34458  cdlemm10N  34602  dihord2pre  34709  dihord4  34742  dihord5b  34743  dihglbcpreN  34784  dihmeetlem13N  34803  dih1dimatlem0  34812  mzpcong  35739  jm2.25lem1  35770  jm2.26  35774  idomsubgmo  35989