Theorem simpl2l 1041

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpl2l	|- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta ) -> ph )

Proof of Theorem simpl2l

Step	Hyp	Ref	Expression
1		simp2l 1014	. 2 |- ( ( ch /\ ( ph /\ ps ) /\ th ) -> ph )
2	1	adantr 465	1 |- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta ) -> ph )

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  6039  omopth2  7044  fin23lem11  8507  dedekind  9554  xaddass  11233  pockthg  13988  gsmsymgreqlem2  15957  efgred  16266  uncon  19055  basqtop  19306  utop2nei  19847  ucncn  19882  cxple2  22164  cxple2a  22166  ax5seglem1  23196  ax5seglem2  23197  axpasch  23209  axcontlem4  23235  cvmlift2lem10  27223  ntrivcvgmul  27439  br4  27590  cgrcomim  28042  btwnintr  28072  btwnouttr2  28075  btwndiff  28080  btwnconn1lem14  28153  btwnconn3  28156  segcon2  28158  brsegle  28161  brsegle2  28162  segleantisym  28168  seglelin  28169  outsideofeu  28184  qirropth  29275  mzpcong  29341  jm2.25lem1  29373  jm2.26  29377  idomsubgmo  29589  wlklniswwlkn1  30359  eqlkr  32840  eqlkr2  32841  lkrlsp  32843  atbtwn  33186  athgt  33196  3dimlem3  33201  3dimlem3OLDN  33202  3dim3  33209  3atlem7  33229  4atlem0a  33333  4atlem3a  33337  4atlem11  33349  lneq2at  33518  lnatexN  33519  cdlemb  33534  paddasslem6  33565  llnexchb2  33609  lhp2lt  33741  lhpexle2lem  33749  lhpexle3  33752  lhpmcvr3  33765  lhpat3  33786  ltrnnidn  33914  ltrneq3  33948  cdleme17b  34027  cdleme25a  34093  cdleme25dN  34096  cdleme27cl  34106  cdlemefrs29bpre0  34136  cdlemefs32sn1aw  34154  cdleme32le  34187  cdleme46f2g2  34233  cdleme46f2g1  34234  cdleme50trn3  34293  trlord  34309  ltrniotavalbN  34324  cdlemg6  34363  cdlemg7N  34366  cdlemg11b  34382  cdlemg15a  34395  cdlemg15  34396  cdlemg39  34456  trlcone  34468  cdlemg42  34469  tendoconid  34569  tendotr  34570  cdlemk39u  34708  cdlemk19u  34710  cdleml5N  34720  cdlemm10N  34859  dihord11b  34963  dihord2pre  34966  dihvalcqpre  34976  dihopelvalcpre  34989  dihord6apre  34997  dihord4  34999  dihord5b  35000  dihglblem5apreN  35032  dihmeetlem13N  35060  dihmeetlem19N  35066  dih1dimatlem0  35069