Theorem simpl12 1073

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

Assertion

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

Proof of Theorem simpl12

Step	Hyp	Ref	Expression
1		simp12 1028	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) -> ps )
2	1	adantr 465	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et ) -> ps )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 974

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 976

This theorem is referenced by:  pythagtriplem4  14325  pmatcollpw1lem1  19253  pmatcollpw1  19255  mp2pm2mplem2  19286  brbtwn2  24186  ax5seg  24219  br8  29161  ifscgr  29670  seglecgr12im  29736  fourierdlem77  31920  lkrshp  34705  atlatle  34920  cvlcvr1  34939  atbtwn  35045  3dimlem3  35060  3dimlem3OLDN  35061  1cvratex  35072  llnmlplnN  35138  4atlem3  35195  4atlem3a  35196  4atlem11  35208  4atlem12  35211  cdlemb  35393  paddasslem4  35422  paddasslem10  35428  pmodlem1  35445  llnexchb2lem  35467  arglem1N  35790  cdlemd4  35801  cdlemd  35807  cdleme16  35885  cdleme20  35925  cdleme21k  35939  cdleme22cN  35943  cdleme27N  35970  cdleme28c  35973  cdleme29ex  35975  cdleme32fva  36038  cdleme40n  36069  cdlemg15a  36256  cdlemg15  36257  cdlemg16ALTN  36259  cdlemg16z  36260  cdlemg20  36286  cdlemg22  36288  cdlemg29  36306  cdlemg38  36316  cdlemk33N  36510  cdlemk56  36572