Theorem simpl2l 1083

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

Syntax hints:   -> wi 4   /\ wa 376   /\ w3a 1007

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 190  df-an 378  df-3an 1009

This theorem is referenced by:  soisores  6236  omopth2  7303  fin23lem11  8765  dedekind  9815  xaddass  11560  swrdsbslen  12858  ntrivcvgmul  14035  pockthg  14929  gsmsymgreqlem2  17150  efgred  17476  decpmatmullem  19872  decpmatmul  19873  uncon  20521  basqtop  20803  utop2nei  21343  ucncn  21378  cxple2  23721  cxple2a  23723  ax5seglem1  25037  ax5seglem2  25038  axpasch  25050  axcontlem4  25076  wlklniswwlkn1  25506  cvmlift2lem10  30107  br4  30469  cgrcomim  30827  btwnintr  30857  btwnouttr2  30860  btwndiff  30865  btwnconn1lem14  30938  btwnconn3  30941  segcon2  30943  brsegle  30946  brsegle2  30947  segleantisym  30953  seglelin  30954  outsideofeu  30969  eqlkr  32736  eqlkr2  32737  lkrlsp  32739  atbtwn  33082  athgt  33092  3dimlem3  33097  3dimlem3OLDN  33098  3dim3  33105  3atlem7  33125  4atlem0a  33229  4atlem3a  33233  4atlem11  33245  lneq2at  33414  lnatexN  33415  cdlemb  33430  paddasslem6  33461  llnexchb2  33505  lhp2lt  33637  lhpexle2lem  33645  lhpexle3  33648  lhpmcvr3  33661  lhpat3  33682  ltrnnidn  33811  ltrneq3  33845  cdleme17b  33924  cdleme25a  33991  cdleme25dN  33994  cdleme27cl  34004  cdlemefrs29bpre0  34034  cdlemefs32sn1aw  34052  cdleme32le  34085  cdleme46f2g2  34131  cdleme46f2g1  34132  cdleme50trn3  34191  trlord  34207  ltrniotavalbN  34222  cdlemg6  34261  cdlemg7N  34264  cdlemg11b  34280  cdlemg15a  34293  cdlemg15  34294  cdlemg39  34354  trlcone  34366  cdlemg42  34367  tendoconid  34467  tendotr  34468  cdlemk39u  34606  cdlemk19u  34608  cdleml5N  34618  cdlemm10N  34757  dihord11b  34861  dihord2pre  34864  dihvalcqpre  34874  dihopelvalcpre  34887  dihord6apre  34895  dihord4  34897  dihord5b  34898  dihglblem5apreN  34930  dihmeetlem13N  34958  dihmeetlem19N  34964  dih1dimatlem0  34967  qirropth  35827  mzpcong  35893  jm2.25lem1  35924  jm2.26  35928  idomsubgmo  36143  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem97  38179  1pthon2v-av  40041