Theorem simpl2r 1048

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

Syntax hints:   -> wi 4   /\ wa 367   /\ w3a 971

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 369  df-3an 973

This theorem is referenced by:  soisores  6198  omopth2  7225  fin23lem11  8688  xmulasslem3  11481  ssfzo12bi  11888  ntrivcvgmul  13793  pockthg  14508  gsmsymgreqlem2  16655  efgred  16965  lspfixed  17969  decpmatmullem  19439  decpmatmul  19440  uncon  20096  llyrest  20152  basqtop  20378  tmdgsum  20760  tsmsxp  20823  ucncn  20954  mulcxp  23234  cxple2  23246  ax5seglem1  24433  ax5seglem2  24434  axpasch  24446  axcontlem4  24472  wlklniswwlkn1  24901  cvmlift2lem10  29021  br4  29428  cgrcomim  29867  btwnintr  29897  btwnouttr2  29900  btwndiff  29905  btwnconn1lem14  29978  btwnconn3  29981  segcon2  29983  brsegle  29986  brsegle2  29987  segleantisym  29993  outsideofeu  30009  mzpcong  31149  jm2.25lem1  31179  jm2.26  31183  idomsubgmo  31396  eqlkr  35221  eqlkr2  35222  lkrlsp  35224  atbtwn  35567  3dimlem3OLDN  35583  3dim3  35590  3atlem7  35610  4atlem0a  35714  4atlem3a  35718  4atlem11  35730  lneq2at  35899  lnatexN  35900  paddasslem6  35946  llnexchb2  35990  lhpexle2lem  36130  lhpexle3  36133  lhp2at0nle  36156  lhpat3  36167  trlnid  36301  ltrneq3  36330  cdleme17b  36409  cdleme27cl  36489  cdlemefrs29bpre0  36519  cdlemefrs29clN  36522  cdlemefrs32fva  36523  cdlemefs32sn1aw  36537  cdleme32le  36570  ltrniotavalbN  36707  cdlemg6  36746  cdlemg7N  36749  cdlemg11b  36765  cdlemg15a  36778  cdlemg15  36779  cdlemg39  36839  trlcone  36851  cdlemg42  36852  tendoconid  36952  tendotr  36953  cdlemk39u  37091  cdlemk19u  37093  tendoex  37098  cdlemm10N  37242  dihord2pre  37349  dihord4  37382  dihord5b  37383  dihglbcpreN  37424  dihmeetlem13N  37443  dih1dimatlem0  37452