Theorem simpl21 1083

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

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  brbtwn2  24877  ax5seglem3a  24902  ax5seg  24910  axpasch  24913  axeuclid  24935  br8d  28164  br8  30347  cgrextend  30724  segconeq  30726  trisegint  30744  ifscgr  30760  cgrsub  30761  cgrxfr  30771  lineext  30792  seglecgr12im  30826  segletr  30830  lineunray  30863  lineelsb2  30864  cvrcmp  32761  cvlatexch3  32816  cvlsupr2  32821  atexchcvrN  32917  3dim1  32944  3dim2  32945  ps-1  32954  ps-2  32955  3atlem3  32962  3atlem5  32964  lplnnle2at  33018  lplnllnneN  33033  2llnjaN  33043  4atlem3  33073  4atlem10b  33082  4atlem12  33089  2llnma3r  33265  paddasslem4  33300  paddasslem7  33303  paddasslem8  33304  paddasslem12  33308  paddasslem13  33309  pmodlem1  33323  pmodlem2  33324  llnexchb2lem  33345  4atex2  33554  ltrnatlw  33661  trlval4  33666  arglem1N  33668  cdlemd4  33679  cdlemd5  33680  cdleme0moN  33703  cdleme16  33763  cdleme20  33803  cdleme21j  33815  cdleme21k  33817  cdleme27N  33848  cdleme28c  33851  cdleme43fsv1snlem  33899  cdleme38n  33943  cdleme40n  33947  cdleme41snaw  33955  cdlemg6c  34099  cdlemg8c  34108  cdlemg8  34110  cdlemg12e  34126  cdlemg16  34136  cdlemg16ALTN  34137  cdlemg16z  34138  cdlemg16zz  34139  cdlemg18a  34157  cdlemg20  34164  cdlemg22  34166  cdlemg37  34168  cdlemg27b  34175  cdlemg31d  34179  cdlemg33  34190  cdlemg38  34194  cdlemg44b  34211  cdlemk38  34394  cdlemk35s-id  34417  cdlemk39s-id  34419  cdlemk55  34440  cdlemk35u  34443  cdlemk55u  34445  cdleml3N  34457  cdlemn11pre  34690