Theorem simpl21 1066

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 1021	. 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 965

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 967

This theorem is referenced by:  brbtwn2  23156  ax5seglem3a  23181  ax5seg  23189  axpasch  23192  axeuclid  23214  br8d  25947  br8  27571  cgrextend  28044  segconeq  28046  trisegint  28064  ifscgr  28080  cgrsub  28081  cgrxfr  28091  lineext  28112  seglecgr12im  28146  segletr  28150  lineunray  28183  lineelsb2  28184  cvrcmp  32933  cvlatexch3  32988  cvlsupr2  32993  atexchcvrN  33089  3dim1  33116  3dim2  33117  ps-1  33126  ps-2  33127  3atlem3  33134  3atlem5  33136  lplnnle2at  33190  lplnllnneN  33205  2llnjaN  33215  4atlem3  33245  4atlem10b  33254  4atlem12  33261  2llnma3r  33437  paddasslem4  33472  paddasslem7  33475  paddasslem8  33476  paddasslem12  33480  paddasslem13  33481  pmodlem1  33495  pmodlem2  33496  llnexchb2lem  33517  4atex2  33726  ltrnatlw  33832  trlval4  33837  arglem1N  33839  cdlemd4  33850  cdlemd5  33851  cdleme0moN  33874  cdleme16  33934  cdleme20  33973  cdleme21j  33985  cdleme21k  33987  cdleme27N  34018  cdleme28c  34021  cdleme43fsv1snlem  34069  cdleme38n  34113  cdleme40n  34117  cdleme41snaw  34125  cdlemg6c  34269  cdlemg8c  34278  cdlemg8  34280  cdlemg12e  34296  cdlemg16  34306  cdlemg16ALTN  34307  cdlemg16z  34308  cdlemg16zz  34309  cdlemg18a  34327  cdlemg20  34334  cdlemg22  34336  cdlemg37  34338  cdlemg27b  34345  cdlemg31d  34349  cdlemg33  34360  cdlemg38  34364  cdlemg44b  34381  cdlemk38  34564  cdlemk35s-id  34587  cdlemk39s-id  34589  cdlemk55  34610  cdlemk35u  34613  cdlemk55u  34615  cdleml3N  34627  cdlemn11pre  34860