Theorem simpl2l 1047

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

Syntax hints:   -> wi 4   /\ wa 367   /\ w3a 971

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 369  df-3an 973

This theorem is referenced by:  soisores  6198  omopth2  7225  fin23lem11  8688  dedekind  9733  xaddass  11444  swrdsbslen  12664  ntrivcvgmul  13793  pockthg  14508  gsmsymgreqlem2  16655  efgred  16965  decpmatmullem  19439  decpmatmul  19440  uncon  20096  basqtop  20378  utop2nei  20919  ucncn  20954  cxple2  23246  cxple2a  23248  ax5seglem1  24433  ax5seglem2  24434  axpasch  24446  axcontlem4  24472  wlklniswwlkn1  24901  cvmlift2lem10  29021  br4  29428  cgrcomim  29867  btwnintr  29897  btwnouttr2  29900  btwndiff  29905  btwnconn1lem14  29978  btwnconn3  29981  segcon2  29983  brsegle  29986  brsegle2  29987  segleantisym  29993  seglelin  29994  outsideofeu  30009  qirropth  31083  mzpcong  31149  jm2.25lem1  31179  jm2.26  31183  idomsubgmo  31396  fourierdlem42  32170  fourierdlem97  32225  eqlkr  35221  eqlkr2  35222  lkrlsp  35224  atbtwn  35567  athgt  35577  3dimlem3  35582  3dimlem3OLDN  35583  3dim3  35590  3atlem7  35610  4atlem0a  35714  4atlem3a  35718  4atlem11  35730  lneq2at  35899  lnatexN  35900  cdlemb  35915  paddasslem6  35946  llnexchb2  35990  lhp2lt  36122  lhpexle2lem  36130  lhpexle3  36133  lhpmcvr3  36146  lhpat3  36167  ltrnnidn  36296  ltrneq3  36330  cdleme17b  36409  cdleme25a  36476  cdleme25dN  36479  cdleme27cl  36489  cdlemefrs29bpre0  36519  cdlemefs32sn1aw  36537  cdleme32le  36570  cdleme46f2g2  36616  cdleme46f2g1  36617  cdleme50trn3  36676  trlord  36692  ltrniotavalbN  36707  cdlemg6  36746  cdlemg7N  36749  cdlemg11b  36765  cdlemg15a  36778  cdlemg15  36779  cdlemg39  36839  trlcone  36851  cdlemg42  36852  tendoconid  36952  tendotr  36953  cdlemk39u  37091  cdlemk19u  37093  cdleml5N  37103  cdlemm10N  37242  dihord11b  37346  dihord2pre  37349  dihvalcqpre  37359  dihopelvalcpre  37372  dihord6apre  37380  dihord4  37382  dihord5b  37383  dihglblem5apreN  37415  dihmeetlem13N  37443  dihmeetlem19N  37449  dih1dimatlem0  37452