Theorem simpl21 1108

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

Syntax hints:   -> wi 4   /\ wa 376   /\ w3a 1007

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 190  df-an 378  df-3an 1009

This theorem is referenced by:  brbtwn2  25014  ax5seglem3a  25039  ax5seg  25047  axpasch  25050  axeuclid  25072  br8d  28294  br8  30467  cgrextend  30846  segconeq  30848  trisegint  30866  ifscgr  30882  cgrsub  30883  cgrxfr  30893  lineext  30914  seglecgr12im  30948  segletr  30952  lineunray  30985  lineelsb2  30986  cvrcmp  32920  cvlatexch3  32975  cvlsupr2  32980  atexchcvrN  33076  3dim1  33103  3dim2  33104  ps-1  33113  ps-2  33114  3atlem3  33121  3atlem5  33123  lplnnle2at  33177  lplnllnneN  33192  2llnjaN  33202  4atlem3  33232  4atlem10b  33241  4atlem12  33248  2llnma3r  33424  paddasslem4  33459  paddasslem7  33462  paddasslem8  33463  paddasslem12  33467  paddasslem13  33468  pmodlem1  33482  pmodlem2  33483  llnexchb2lem  33504  4atex2  33713  ltrnatlw  33820  trlval4  33825  arglem1N  33827  cdlemd4  33838  cdlemd5  33839  cdleme0moN  33862  cdleme16  33922  cdleme20  33962  cdleme21j  33974  cdleme21k  33976  cdleme27N  34007  cdleme28c  34010  cdleme43fsv1snlem  34058  cdleme38n  34102  cdleme40n  34106  cdleme41snaw  34114  cdlemg6c  34258  cdlemg8c  34267  cdlemg8  34269  cdlemg12e  34285  cdlemg16  34295  cdlemg16ALTN  34296  cdlemg16z  34297  cdlemg16zz  34298  cdlemg18a  34316  cdlemg20  34323  cdlemg22  34325  cdlemg37  34327  cdlemg27b  34334  cdlemg31d  34338  cdlemg33  34349  cdlemg38  34353  cdlemg44b  34370  cdlemk38  34553  cdlemk35s-id  34576  cdlemk39s-id  34578  cdlemk55  34599  cdlemk35u  34602  cdlemk55u  34604  cdleml3N  34616  cdlemn11pre  34849