Theorem simpl2r 1084

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

Syntax hints:   -> wi 4   /\ wa 376   /\ w3a 1007

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 190  df-an 378  df-3an 1009

This theorem is referenced by:  soisores  6236  omopth2  7303  fin23lem11  8765  xmulasslem3  11597  ssfzo12bi  12035  ntrivcvgmul  14035  pockthg  14929  gsmsymgreqlem2  17150  efgred  17476  lspfixed  18429  decpmatmullem  19872  decpmatmul  19873  uncon  20521  llyrest  20577  basqtop  20803  tmdgsum  21188  tsmsxp  21247  ucncn  21378  mulcxp  23709  cxple2  23721  ax5seglem1  25037  ax5seglem2  25038  axpasch  25050  axcontlem4  25076  wlklniswwlkn1  25506  cvmlift2lem10  30107  br4  30469  cgrcomim  30827  btwnintr  30857  btwnouttr2  30860  btwndiff  30865  btwnconn1lem14  30938  btwnconn3  30941  segcon2  30943  brsegle  30946  brsegle2  30947  segleantisym  30953  outsideofeu  30969  eqlkr  32736  eqlkr2  32737  lkrlsp  32739  atbtwn  33082  3dimlem3OLDN  33098  3dim3  33105  3atlem7  33125  4atlem0a  33229  4atlem3a  33233  4atlem11  33245  lneq2at  33414  lnatexN  33415  paddasslem6  33461  llnexchb2  33505  lhpexle2lem  33645  lhpexle3  33648  lhp2at0nle  33671  lhpat3  33682  trlnid  33816  ltrneq3  33845  cdleme17b  33924  cdleme27cl  34004  cdlemefrs29bpre0  34034  cdlemefrs29clN  34037  cdlemefrs32fva  34038  cdlemefs32sn1aw  34052  cdleme32le  34085  ltrniotavalbN  34222  cdlemg6  34261  cdlemg7N  34264  cdlemg11b  34280  cdlemg15a  34293  cdlemg15  34294  cdlemg39  34354  trlcone  34366  cdlemg42  34367  tendoconid  34467  tendotr  34468  cdlemk39u  34606  cdlemk19u  34608  tendoex  34613  cdlemm10N  34757  dihord2pre  34864  dihord4  34897  dihord5b  34898  dihglbcpreN  34939  dihmeetlem13N  34958  dih1dimatlem0  34967  mzpcong  35893  jm2.25lem1  35924  jm2.26  35928  idomsubgmo  36143  1pthon2v-av  40041