Theorem simpl3r 1117

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpl3r	|- ( ( ( ch /\ th /\ ( ph /\ ps ) ) /\ ta ) -> ps )

Proof of Theorem simpl3r

Step	Hyp	Ref	Expression
1		simp3r 1090	. 2 |- ( ( ch /\ th /\ ( ph /\ ps ) ) -> ps )
2	1	adantr 481	1 |- ( ( ( ch /\ th /\ ( ph /\ ps ) ) /\ ta ) -> ps )

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:  tfisi  7058  omopth2  7664  ltmul1a  10872  xmulasslem3  12116  xadddi2  12127  swrdsbslen  13448  swrdspsleq  13449  dvdsadd2b  15028  pockthg  15610  psgnunilem4  17917  efgred  18161  marrepeval  20369  submaeval  20388  mdetmul  20429  minmar1eval  20455  ptbasin  21380  basqtop  21514  xrsmopn  22615  axpasch  25821  axeuclid  25843  br4  31648  nosupbnd1lem3  31856  nosupbnd1lem4  31857  nosupbnd1lem5  31858  btwnouttr2  32129  trisegint  32135  cgrxfr  32162  lineext  32183  btwnconn1lem13  32206  btwnconn1lem14  32207  btwnconn3  32210  brsegle  32215  brsegle2  32216  segleantisym  32222  outsideofeu  32238  lineunray  32254  lineelsb2  32255  cvrcmp  34570  atcvrj2b  34718  3dimlem3  34747  3dimlem3OLDN  34748  3dim3  34755  ps-1  34763  ps-2  34764  lplnnle2at  34827  2llnm3N  34855  4atlem0a  34879  4atlem3  34882  4atlem3a  34883  lnatexN  35065  paddasslem8  35113  paddasslem9  35114  paddasslem10  35115  paddasslem12  35117  paddasslem13  35118  lhpexle2lem  35295  lhpexle3  35298  lhpat3  35332  4atex  35362  trlval2  35450  trlval4  35475  cdleme16  35572  cdleme21  35625  cdleme21k  35626  cdleme27cl  35654  cdleme27N  35657  cdleme43fsv1snlem  35708  cdleme48fvg  35788  cdlemg8  35919  cdlemg15a  35943  cdlemg16z  35947  cdlemg24  35976  cdlemg38  36003  cdlemg40  36005  trlcone  36016  cdlemj2  36110  tendoid0  36113  tendoconid  36117  cdlemk34  36198  cdlemk38  36203  cdlemkid4  36222  cdlemk53  36245  tendospcanN  36312  dihvalcqpre  36524  dihmeetlem15N  36610  qirropth  37473  mzpcong  37539  jm2.26  37569  aomclem6  37629  islptre  39851  limccog  39852  limcleqr  39876  fourierdlem42  40366  elaa2  40451