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  24335  ax5seglem3a  24360  ax5seg  24368  axpasch  24371  axeuclid  24393  br8d  27606  br8  29403  cgrextend  29863  segconeq  29865  trisegint  29883  ifscgr  29899  cgrsub  29900  cgrxfr  29910  lineext  29931  seglecgr12im  29965  segletr  29969  lineunray  30002  lineelsb2  30003  cvrcmp  35151  cvlatexch3  35206  cvlsupr2  35211  atexchcvrN  35307  3dim1  35334  3dim2  35335  ps-1  35344  ps-2  35345  3atlem3  35352  3atlem5  35354  lplnnle2at  35408  lplnllnneN  35423  2llnjaN  35433  4atlem3  35463  4atlem10b  35472  4atlem12  35479  2llnma3r  35655  paddasslem4  35690  paddasslem7  35693  paddasslem8  35694  paddasslem12  35698  paddasslem13  35699  pmodlem1  35713  pmodlem2  35714  llnexchb2lem  35735  4atex2  35944  ltrnatlw  36051  trlval4  36056  arglem1N  36058  cdlemd4  36069  cdlemd5  36070  cdleme0moN  36093  cdleme16  36153  cdleme20  36193  cdleme21j  36205  cdleme21k  36207  cdleme27N  36238  cdleme28c  36241  cdleme43fsv1snlem  36289  cdleme38n  36333  cdleme40n  36337  cdleme41snaw  36345  cdlemg6c  36489  cdlemg8c  36498  cdlemg8  36500  cdlemg12e  36516  cdlemg16  36526  cdlemg16ALTN  36527  cdlemg16z  36528  cdlemg16zz  36529  cdlemg18a  36547  cdlemg20  36554  cdlemg22  36556  cdlemg37  36558  cdlemg27b  36565  cdlemg31d  36569  cdlemg33  36580  cdlemg38  36584  cdlemg44b  36601  cdlemk38  36784  cdlemk35s-id  36807  cdlemk39s-id  36809  cdlemk55  36830  cdlemk35u  36833  cdlemk55u  36835  cdleml3N  36847  cdlemn11pre  37080