Theorem simpl23 1141

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

Assertion

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

Proof of Theorem simpl23

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

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:  mulgdirlem  17572  brbtwn2  25785  ax5seglem3a  25810  ax5seg  25818  axpasch  25821  axeuclid  25843  br8d  29422  br8  31646  nosupbnd2lem1  31861  cgrextend  32115  segconeq  32117  segconeu  32118  trisegint  32135  ifscgr  32151  cgrsub  32152  cgrxfr  32162  lineext  32183  seglecgr12im  32217  segletr  32221  lineunray  32254  lineelsb2  32255  cvrcmp  34570  cvlsupr2  34630  atcvrj2b  34718  atexchcvrN  34726  3atlem3  34771  3atlem5  34773  lplnnle2at  34827  lplnllnneN  34842  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  arglem1N  35477  cdlemd4  35488  cdlemd5  35489  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  cdlemg16ALTN  35946  cdlemg16zz  35948  cdlemg18a  35966  cdlemg20  35973  cdlemg22  35975  cdlemg37  35977  cdlemg31d  35988  cdlemg33  35999  cdlemg38  36003  cdlemg44b  36020  cdlemk33N  36197  cdlemk34  36198  cdlemk38  36203  cdlemk35s-id  36226  cdlemk39s-id  36228  cdlemk53b  36244  cdlemk53  36245  cdlemk55  36249  cdlemk35u  36252  cdlemk55u  36254  cdleml3N  36266  cdlemn11pre  36499