Theorem simpl2r 1037

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 1010	. 2 |- ( ( ch /\ ( ph /\ ps ) /\ th ) -> ps )
2	1	adantr 462	1 |- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 960

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 962

This theorem is referenced by:  soisores  6015  omopth2  7019  fin23lem11  8482  xmulasslem3  11245  ssfzo12bi  11618  pockthg  13963  gsmsymgreqlem2  15929  efgred  16238  lspfixed  17187  uncon  18992  llyrest  19048  basqtop  19243  tmdgsum  19625  tsmsxp  19688  ucncn  19819  mulcxp  22089  cxple2  22101  ax5seglem1  23109  ax5seglem2  23110  axpasch  23122  axcontlem4  23148  cvmlift2lem10  27131  ntrivcvgmul  27346  br4  27497  cgrcomim  27949  btwnintr  27979  btwnouttr2  27982  btwndiff  27987  btwnconn1lem14  28060  btwnconn3  28063  segcon2  28065  brsegle  28068  brsegle2  28069  segleantisym  28075  outsideofeu  28091  mzpcong  29240  jm2.25lem1  29272  jm2.26  29276  idomsubgmo  29488  wlklniswwlkn1  30258  eqlkr  32466  eqlkr2  32467  lkrlsp  32469  atbtwn  32812  3dimlem3OLDN  32828  3dim3  32835  3atlem7  32855  4atlem0a  32959  4atlem3a  32963  4atlem11  32975  lneq2at  33144  lnatexN  33145  paddasslem6  33191  llnexchb2  33235  lhpexle2lem  33375  lhpexle3  33378  lhp2at0nle  33401  lhpat3  33412  trlnid  33545  ltrneq3  33574  cdleme17b  33653  cdleme27cl  33732  cdlemefrs29bpre0  33762  cdlemefrs29clN  33765  cdlemefrs32fva  33766  cdlemefs32sn1aw  33780  cdleme32le  33813  ltrniotavalbN  33950  cdlemg6  33989  cdlemg7N  33992  cdlemg11b  34008  cdlemg15a  34021  cdlemg15  34022  cdlemg39  34082  trlcone  34094  cdlemg42  34095  tendoconid  34195  tendotr  34196  cdlemk39u  34334  cdlemk19u  34336  tendoex  34341  cdlemm10N  34485  dihord2pre  34592  dihord4  34625  dihord5b  34626  dihglbcpreN  34667  dihmeetlem13N  34686  dih1dimatlem0  34695