Theorem simpl22 1140

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

Assertion

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

Proof of Theorem simpl22

Step	Hyp	Ref	Expression
1		simp22 1095	. 2 |- ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) -> ps )
2	1	adantr 481	1 |- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ et ) -> ps )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  brbtwn2  25785  ax5seg  25818  axpasch  25821  axeuclid  25843  br8d  29422  br8  31646  cgrextend  32115  segconeq  32117  trisegint  32135  ifscgr  32151  cgrsub  32152  cgrxfr  32162  lineext  32183  seglecgr12im  32217  segletr  32221  lineunray  32254  lineelsb2  32255  cvrcmp  34570  cvlatexch3  34625  cvlsupr2  34630  atcvrj2b  34718  atexchcvrN  34726  3dim1  34753  3dim2  34754  3atlem3  34771  3atlem5  34773  lplnnle2at  34827  2llnjaN  34852  4atlem3  34882  4atlem10b  34891  4atlem12  34898  2llnma3r  35074  paddasslem4  35109  paddasslem7  35112  paddasslem8  35113  paddasslem12  35117  paddasslem13  35118  paddasslem15  35120  pmodlem1  35132  pmodlem2  35133  atmod1i1m  35144  llnexchb2lem  35154  4atex2  35363  ltrnatlw  35470  trlval4  35475  arglem1N  35477  cdlemd4  35488  cdlemd5  35489  cdleme0moN  35512  cdleme16  35572  cdleme20  35612  cdleme21k  35626  cdleme27N  35657  cdleme28c  35660  cdleme43fsv1snlem  35708  cdleme38n  35752  cdleme40n  35756  cdleme41snaw  35764  cdlemg6c  35908  cdlemg8c  35917  cdlemg8  35919  cdlemg12e  35935  cdlemg16  35945  cdlemg16ALTN  35946  cdlemg16z  35947  cdlemg16zz  35948  cdlemg18a  35966  cdlemg20  35973  cdlemg22  35975  cdlemg37  35977  cdlemg31d  35988  cdlemg33  35999  cdlemg38  36003  cdlemg44b  36020  cdlemk38  36203  cdlemk35s-id  36226  cdlemk39s-id  36228  cdlemk53b  36244  cdlemk55  36249  cdlemk35u  36252  cdlemk55u  36254  cdlemn11pre  36499