Theorem simpl12 1082

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

Syntax hints:   -> wi 4   /\ wa 371   /\ w3a 983

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 189  df-an 373  df-3an 985

This theorem is referenced by:  pythagtriplem4  14766  pmatcollpw1lem1  19794  pmatcollpw1  19796  mp2pm2mplem2  19827  brbtwn2  24931  ax5seg  24964  br8  30401  ifscgr  30814  seglecgr12im  30880  lkrshp  32638  atlatle  32853  cvlcvr1  32872  atbtwn  32978  3dimlem3  32993  3dimlem3OLDN  32994  1cvratex  33005  llnmlplnN  33071  4atlem3  33128  4atlem3a  33129  4atlem11  33141  4atlem12  33144  cdlemb  33326  paddasslem4  33355  paddasslem10  33361  pmodlem1  33378  llnexchb2lem  33400  arglem1N  33723  cdlemd4  33734  cdlemd  33740  cdleme16  33818  cdleme20  33858  cdleme21k  33872  cdleme22cN  33876  cdleme27N  33903  cdleme28c  33906  cdleme29ex  33908  cdleme32fva  33971  cdleme40n  34002  cdlemg15a  34189  cdlemg15  34190  cdlemg16ALTN  34192  cdlemg16z  34193  cdlemg20  34219  cdlemg22  34221  cdlemg29  34239  cdlemg38  34249  cdlemk33N  34443  cdlemk56  34505  fourierdlem77  37915