Theorem simpl2r 1011

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

Syntax hints:   -> wi 4   /\ wa 359   /\ w3a 936

This theorem is referenced by:  soisores  6006  omopth2  6786  fin23lem11  8153  xmulasslem3  10821  pockthg  13229  efgred  15335  lspfixed  16155  uncon  17445  llyrest  17501  basqtop  17696  tmdgsum  18078  tsmsxp  18137  ucncn  18268  mulcxp  20529  cxple2  20541  cvmlift2lem10  24952  ntrivcvgmul  25183  br4  25329  ax5seglem1  25771  ax5seglem2  25772  axpasch  25784  axcontlem4  25810  cgrcomim  25827  btwnintr  25857  btwnouttr2  25860  btwndiff  25865  btwnconn1lem14  25938  btwnconn3  25941  segcon2  25943  brsegle  25946  brsegle2  25947  segleantisym  25953  outsideofeu  25969  mzpcong  26927  jm2.25lem1  26959  jm2.26  26963  idomsubgmo  27382  eqlkr  29582  eqlkr2  29583  lkrlsp  29585  atbtwn  29928  3dimlem3OLDN  29944  3dim3  29951  3atlem7  29971  4atlem0a  30075  4atlem3a  30079  4atlem11  30091  lneq2at  30260  lnatexN  30261  paddasslem6  30307  llnexchb2  30351  lhpexle2lem  30491  lhpexle3  30494  lhp2at0nle  30517  lhpat3  30528  trlnid  30661  ltrneq3  30690  cdleme17b  30769  cdleme27cl  30848  cdlemefrs29bpre0  30878  cdlemefrs29clN  30881  cdlemefrs32fva  30882  cdlemefs32sn1aw  30896  cdleme32le  30929  ltrniotavalbN  31066  cdlemg6  31105  cdlemg7N  31108  cdlemg11b  31124  cdlemg15a  31137  cdlemg15  31138  cdlemg39  31198  trlcone  31210  cdlemg42  31211  tendoconid  31311  tendotr  31312  cdlemk39u  31450  cdlemk19u  31452  tendoex  31457  cdlemm10N  31601  dihord2pre  31708  dihord4  31741  dihord5b  31742  dihglbcpreN  31783  dihmeetlem13N  31802  dih1dimatlem0  31811

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938