Theorem simpl2l 1049

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

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  6211  omopth2  7233  fin23lem11  8697  dedekind  9743  xaddass  11441  pockthg  14283  gsmsymgreqlem2  16261  efgred  16572  decpmatmullem  19067  decpmatmul  19068  uncon  19724  basqtop  19975  utop2nei  20516  ucncn  20551  cxple2  22834  cxple2a  22836  ax5seglem1  23935  ax5seglem2  23936  axpasch  23948  axcontlem4  23974  wlklniswwlkn1  24403  cvmlift2lem10  28425  ntrivcvgmul  28641  br4  28792  cgrcomim  29244  btwnintr  29274  btwnouttr2  29277  btwndiff  29282  btwnconn1lem14  29355  btwnconn3  29358  segcon2  29360  brsegle  29363  brsegle2  29364  segleantisym  29370  seglelin  29371  outsideofeu  29386  qirropth  30476  mzpcong  30542  jm2.25lem1  30572  jm2.26  30576  idomsubgmo  30788  fourierdlem42  31477  fourierdlem97  31532  eqlkr  33914  eqlkr2  33915  lkrlsp  33917  atbtwn  34260  athgt  34270  3dimlem3  34275  3dimlem3OLDN  34276  3dim3  34283  3atlem7  34303  4atlem0a  34407  4atlem3a  34411  4atlem11  34423  lneq2at  34592  lnatexN  34593  cdlemb  34608  paddasslem6  34639  llnexchb2  34683  lhp2lt  34815  lhpexle2lem  34823  lhpexle3  34826  lhpmcvr3  34839  lhpat3  34860  ltrnnidn  34988  ltrneq3  35022  cdleme17b  35101  cdleme25a  35167  cdleme25dN  35170  cdleme27cl  35180  cdlemefrs29bpre0  35210  cdlemefs32sn1aw  35228  cdleme32le  35261  cdleme46f2g2  35307  cdleme46f2g1  35308  cdleme50trn3  35367  trlord  35383  ltrniotavalbN  35398  cdlemg6  35437  cdlemg7N  35440  cdlemg11b  35456  cdlemg15a  35469  cdlemg15  35470  cdlemg39  35530  trlcone  35542  cdlemg42  35543  tendoconid  35643  tendotr  35644  cdlemk39u  35782  cdlemk19u  35784  cdleml5N  35794  cdlemm10N  35933  dihord11b  36037  dihord2pre  36040  dihvalcqpre  36050  dihopelvalcpre  36063  dihord6apre  36071  dihord4  36073  dihord5b  36074  dihglblem5apreN  36106  dihmeetlem13N  36134  dihmeetlem19N  36140  dih1dimatlem0  36143