Theorem simpl21 1074

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

Assertion

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

Proof of Theorem simpl21

Step	Hyp	Ref	Expression
1		simp21 1029	. 2 |- ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) -> ph )
2	1	adantr 465	1 |- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ et ) -> ph )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 973

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 371  df-3an 975

This theorem is referenced by:  brbtwn2  23912  ax5seglem3a  23937  ax5seg  23945  axpasch  23948  axeuclid  23970  br8d  27164  br8  28790  cgrextend  29263  segconeq  29265  trisegint  29283  ifscgr  29299  cgrsub  29300  cgrxfr  29310  lineext  29331  seglecgr12im  29365  segletr  29369  lineunray  29402  lineelsb2  29403  cvrcmp  34098  cvlatexch3  34153  cvlsupr2  34158  atexchcvrN  34254  3dim1  34281  3dim2  34282  ps-1  34291  ps-2  34292  3atlem3  34299  3atlem5  34301  lplnnle2at  34355  lplnllnneN  34370  2llnjaN  34380  4atlem3  34410  4atlem10b  34419  4atlem12  34426  2llnma3r  34602  paddasslem4  34637  paddasslem7  34640  paddasslem8  34641  paddasslem12  34645  paddasslem13  34646  pmodlem1  34660  pmodlem2  34661  llnexchb2lem  34682  4atex2  34891  ltrnatlw  34997  trlval4  35002  arglem1N  35004  cdlemd4  35015  cdlemd5  35016  cdleme0moN  35039  cdleme16  35099  cdleme20  35138  cdleme21j  35150  cdleme21k  35152  cdleme27N  35183  cdleme28c  35186  cdleme43fsv1snlem  35234  cdleme38n  35278  cdleme40n  35282  cdleme41snaw  35290  cdlemg6c  35434  cdlemg8c  35443  cdlemg8  35445  cdlemg12e  35461  cdlemg16  35471  cdlemg16ALTN  35472  cdlemg16z  35473  cdlemg16zz  35474  cdlemg18a  35492  cdlemg20  35499  cdlemg22  35501  cdlemg37  35503  cdlemg27b  35510  cdlemg31d  35514  cdlemg33  35525  cdlemg38  35529  cdlemg44b  35546  cdlemk38  35729  cdlemk35s-id  35752  cdlemk39s-id  35754  cdlemk55  35775  cdlemk35u  35778  cdlemk55u  35780  cdleml3N  35792  cdlemn11pre  36025