Theorem simpl2l 1114

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

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  soisores  6577  omopth2  7664  fin23lem11  9139  dedekind  10200  xaddass  12079  swrdsbslen  13448  ntrivcvgmul  14634  pockthg  15610  gsmsymgreqlem2  17851  efgred  18161  decpmatmullem  20576  decpmatmul  20577  unconn  21232  basqtop  21514  utop2nei  22054  ucncn  22089  cxple2  24443  cxple2a  24445  ax5seglem1  25808  ax5seglem2  25809  axpasch  25821  axcontlem4  25847  1pthon2v  27013  cvmlift2lem10  31294  br4  31648  nolt02o  31845  nosupbnd1lem1  31854  nosupbnd1lem3  31856  nosupbnd1lem4  31857  nosupbnd1lem5  31858  cgrcomim  32096  btwnintr  32126  btwnouttr2  32129  btwndiff  32134  btwnconn1lem14  32207  btwnconn3  32210  segcon2  32212  brsegle  32215  brsegle2  32216  segleantisym  32222  seglelin  32223  outsideofeu  32238  eqlkr  34386  eqlkr2  34387  lkrlsp  34389  atbtwn  34732  athgt  34742  3dimlem3  34747  3dimlem3OLDN  34748  3dim3  34755  3atlem7  34775  4atlem0a  34879  4atlem3a  34883  4atlem11  34895  lneq2at  35064  lnatexN  35065  cdlemb  35080  paddasslem6  35111  llnexchb2  35155  lhp2lt  35287  lhpexle2lem  35295  lhpexle3  35298  lhpmcvr3  35311  lhpat3  35332  ltrnnidn  35461  ltrneq3  35495  cdleme17b  35574  cdleme25a  35641  cdleme25dN  35644  cdleme27cl  35654  cdlemefrs29bpre0  35684  cdlemefs32sn1aw  35702  cdleme32le  35735  cdleme46f2g2  35781  cdleme46f2g1  35782  cdleme50trn3  35841  trlord  35857  ltrniotavalbN  35872  cdlemg6  35911  cdlemg7N  35914  cdlemg11b  35930  cdlemg15a  35943  cdlemg15  35944  cdlemg39  36004  trlcone  36016  cdlemg42  36017  tendoconid  36117  tendotr  36118  cdlemk39u  36256  cdlemk19u  36258  cdleml5N  36268  cdlemm10N  36407  dihord11b  36511  dihord2pre  36514  dihvalcqpre  36524  dihopelvalcpre  36537  dihord6apre  36545  dihord4  36547  dihord5b  36548  dihglblem5apreN  36580  dihmeetlem13N  36608  dihmeetlem19N  36614  dih1dimatlem0  36617  qirropth  37473  mzpcong  37539  jm2.25lem1  37565  jm2.26  37569  idomsubgmo  37776  fourierdlem42  40366  fourierdlem97  40420