Theorem simpl2l 1058

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

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  soisores  6229  omopth2  7289  fin23lem11  8747  dedekind  9797  xaddass  11535  swrdsbslen  12792  ntrivcvgmul  13943  pockthg  14835  gsmsymgreqlem2  17057  efgred  17383  decpmatmullem  19779  decpmatmul  19780  uncon  20428  basqtop  20710  utop2nei  21249  ucncn  21284  cxple2  23626  cxple2a  23628  ax5seglem1  24942  ax5seglem2  24943  axpasch  24955  axcontlem4  24981  wlklniswwlkn1  25410  cvmlift2lem10  30028  br4  30390  cgrcomim  30746  btwnintr  30776  btwnouttr2  30779  btwndiff  30784  btwnconn1lem14  30857  btwnconn3  30860  segcon2  30862  brsegle  30865  brsegle2  30866  segleantisym  30872  seglelin  30873  outsideofeu  30888  eqlkr  32581  eqlkr2  32582  lkrlsp  32584  atbtwn  32927  athgt  32937  3dimlem3  32942  3dimlem3OLDN  32943  3dim3  32950  3atlem7  32970  4atlem0a  33074  4atlem3a  33078  4atlem11  33090  lneq2at  33259  lnatexN  33260  cdlemb  33275  paddasslem6  33306  llnexchb2  33350  lhp2lt  33482  lhpexle2lem  33490  lhpexle3  33493  lhpmcvr3  33506  lhpat3  33527  ltrnnidn  33656  ltrneq3  33690  cdleme17b  33769  cdleme25a  33836  cdleme25dN  33839  cdleme27cl  33849  cdlemefrs29bpre0  33879  cdlemefs32sn1aw  33897  cdleme32le  33930  cdleme46f2g2  33976  cdleme46f2g1  33977  cdleme50trn3  34036  trlord  34052  ltrniotavalbN  34067  cdlemg6  34106  cdlemg7N  34109  cdlemg11b  34125  cdlemg15a  34138  cdlemg15  34139  cdlemg39  34199  trlcone  34211  cdlemg42  34212  tendoconid  34312  tendotr  34313  cdlemk39u  34451  cdlemk19u  34453  cdleml5N  34463  cdlemm10N  34602  dihord11b  34706  dihord2pre  34709  dihvalcqpre  34719  dihopelvalcpre  34732  dihord6apre  34740  dihord4  34742  dihord5b  34743  dihglblem5apreN  34775  dihmeetlem13N  34803  dihmeetlem19N  34809  dih1dimatlem0  34812  qirropth  35673  mzpcong  35739  jm2.25lem1  35770  jm2.26  35774  idomsubgmo  35989  fourierdlem42  37829  fourierdlem42OLD  37830  fourierdlem97  37884