Theorem simpl2r 1042

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

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

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 967

This theorem is referenced by:  soisores  6033  omopth2  7038  fin23lem11  8501  xmulasslem3  11264  ssfzo12bi  11637  pockthg  13982  gsmsymgreqlem2  15951  efgred  16260  lspfixed  17224  uncon  19048  llyrest  19104  basqtop  19299  tmdgsum  19681  tsmsxp  19744  ucncn  19875  mulcxp  22145  cxple2  22157  ax5seglem1  23189  ax5seglem2  23190  axpasch  23202  axcontlem4  23228  cvmlift2lem10  27216  ntrivcvgmul  27432  br4  27583  cgrcomim  28035  btwnintr  28065  btwnouttr2  28068  btwndiff  28073  btwnconn1lem14  28146  btwnconn3  28149  segcon2  28151  brsegle  28154  brsegle2  28155  segleantisym  28161  outsideofeu  28177  mzpcong  29334  jm2.25lem1  29366  jm2.26  29370  idomsubgmo  29582  wlklniswwlkn1  30352  eqlkr  32763  eqlkr2  32764  lkrlsp  32766  atbtwn  33109  3dimlem3OLDN  33125  3dim3  33132  3atlem7  33152  4atlem0a  33256  4atlem3a  33260  4atlem11  33272  lneq2at  33441  lnatexN  33442  paddasslem6  33488  llnexchb2  33532  lhpexle2lem  33672  lhpexle3  33675  lhp2at0nle  33698  lhpat3  33709  trlnid  33842  ltrneq3  33871  cdleme17b  33950  cdleme27cl  34029  cdlemefrs29bpre0  34059  cdlemefrs29clN  34062  cdlemefrs32fva  34063  cdlemefs32sn1aw  34077  cdleme32le  34110  ltrniotavalbN  34247  cdlemg6  34286  cdlemg7N  34289  cdlemg11b  34305  cdlemg15a  34318  cdlemg15  34319  cdlemg39  34379  trlcone  34391  cdlemg42  34392  tendoconid  34492  tendotr  34493  cdlemk39u  34631  cdlemk19u  34633  tendoex  34638  cdlemm10N  34782  dihord2pre  34889  dihord4  34922  dihord5b  34923  dihglbcpreN  34964  dihmeetlem13N  34983  dih1dimatlem0  34992