Theorem simpl2r 1050

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

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

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 975

This theorem is referenced by:  soisores  6209  omopth2  7230  fin23lem11  8693  xmulasslem3  11474  ssfzo12bi  11871  pockthg  14279  gsmsymgreqlem2  16251  efgred  16562  lspfixed  17557  decpmatmullem  19039  decpmatmul  19040  uncon  19696  llyrest  19752  basqtop  19947  tmdgsum  20329  tsmsxp  20392  ucncn  20523  mulcxp  22794  cxple2  22806  ax5seglem1  23907  ax5seglem2  23908  axpasch  23920  axcontlem4  23946  wlklniswwlkn1  24375  cvmlift2lem10  28397  ntrivcvgmul  28613  br4  28764  cgrcomim  29216  btwnintr  29246  btwnouttr2  29249  btwndiff  29254  btwnconn1lem14  29327  btwnconn3  29330  segcon2  29332  brsegle  29335  brsegle2  29336  segleantisym  29342  outsideofeu  29358  mzpcong  30514  jm2.25lem1  30544  jm2.26  30548  idomsubgmo  30760  eqlkr  33896  eqlkr2  33897  lkrlsp  33899  atbtwn  34242  3dimlem3OLDN  34258  3dim3  34265  3atlem7  34285  4atlem0a  34389  4atlem3a  34393  4atlem11  34405  lneq2at  34574  lnatexN  34575  paddasslem6  34621  llnexchb2  34665  lhpexle2lem  34805  lhpexle3  34808  lhp2at0nle  34831  lhpat3  34842  trlnid  34975  ltrneq3  35004  cdleme17b  35083  cdleme27cl  35162  cdlemefrs29bpre0  35192  cdlemefrs29clN  35195  cdlemefrs32fva  35196  cdlemefs32sn1aw  35210  cdleme32le  35243  ltrniotavalbN  35380  cdlemg6  35419  cdlemg7N  35422  cdlemg11b  35438  cdlemg15a  35451  cdlemg15  35452  cdlemg39  35512  trlcone  35524  cdlemg42  35525  tendoconid  35625  tendotr  35626  cdlemk39u  35764  cdlemk19u  35766  tendoex  35771  cdlemm10N  35915  dihord2pre  36022  dihord4  36055  dihord5b  36056  dihglbcpreN  36097  dihmeetlem13N  36116  dih1dimatlem0  36125