Theorem simpl2l 1061

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

Syntax hints:   -> wi 4   /\ wa 371   /\ w3a 985

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 189  df-an 373  df-3an 987

This theorem is referenced by:  soisores  6218  omopth2  7285  fin23lem11  8747  dedekind  9797  xaddass  11535  swrdsbslen  12804  ntrivcvgmul  13958  pockthg  14850  gsmsymgreqlem2  17072  efgred  17398  decpmatmullem  19795  decpmatmul  19796  uncon  20444  basqtop  20726  utop2nei  21265  ucncn  21300  cxple2  23642  cxple2a  23644  ax5seglem1  24958  ax5seglem2  24959  axpasch  24971  axcontlem4  24997  wlklniswwlkn1  25427  cvmlift2lem10  30035  br4  30398  cgrcomim  30756  btwnintr  30786  btwnouttr2  30789  btwndiff  30794  btwnconn1lem14  30867  btwnconn3  30870  segcon2  30872  brsegle  30875  brsegle2  30876  segleantisym  30882  seglelin  30883  outsideofeu  30898  eqlkr  32665  eqlkr2  32666  lkrlsp  32668  atbtwn  33011  athgt  33021  3dimlem3  33026  3dimlem3OLDN  33027  3dim3  33034  3atlem7  33054  4atlem0a  33158  4atlem3a  33162  4atlem11  33174  lneq2at  33343  lnatexN  33344  cdlemb  33359  paddasslem6  33390  llnexchb2  33434  lhp2lt  33566  lhpexle2lem  33574  lhpexle3  33577  lhpmcvr3  33590  lhpat3  33611  ltrnnidn  33740  ltrneq3  33774  cdleme17b  33853  cdleme25a  33920  cdleme25dN  33923  cdleme27cl  33933  cdlemefrs29bpre0  33963  cdlemefs32sn1aw  33981  cdleme32le  34014  cdleme46f2g2  34060  cdleme46f2g1  34061  cdleme50trn3  34120  trlord  34136  ltrniotavalbN  34151  cdlemg6  34190  cdlemg7N  34193  cdlemg11b  34209  cdlemg15a  34222  cdlemg15  34223  cdlemg39  34283  trlcone  34295  cdlemg42  34296  tendoconid  34396  tendotr  34397  cdlemk39u  34535  cdlemk19u  34537  cdleml5N  34547  cdlemm10N  34686  dihord11b  34790  dihord2pre  34793  dihvalcqpre  34803  dihopelvalcpre  34816  dihord6apre  34824  dihord4  34826  dihord5b  34827  dihglblem5apreN  34859  dihmeetlem13N  34887  dihmeetlem19N  34893  dih1dimatlem0  34896  qirropth  35756  mzpcong  35822  jm2.25lem1  35853  jm2.26  35857  idomsubgmo  36072  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem97  38067