Theorem simpl12 1072

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 1027	. 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 973

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 975

This theorem is referenced by:  pythagtriplem4  14195  pmatcollpw1lem1  19039  pmatcollpw1  19041  mp2pm2mplem2  19072  brbtwn2  23881  ax5seg  23914  br8  28759  ifscgr  29268  seglecgr12im  29334  fourierdlem77  31484  lkrshp  33902  atlatle  34117  cvlcvr1  34136  atbtwn  34242  3dimlem3  34257  3dimlem3OLDN  34258  1cvratex  34269  llnmlplnN  34335  4atlem3  34392  4atlem3a  34393  4atlem11  34405  4atlem12  34408  cdlemb  34590  paddasslem4  34619  paddasslem10  34625  pmodlem1  34642  llnexchb2lem  34664  arglem1N  34986  cdlemd4  34997  cdlemd  35003  cdleme16  35081  cdleme20  35120  cdleme21k  35134  cdleme22cN  35138  cdleme27N  35165  cdleme28c  35168  cdleme29ex  35170  cdleme32fva  35233  cdleme40n  35264  cdlemg15a  35451  cdlemg15  35452  cdlemg16ALTN  35454  cdlemg16z  35455  cdlemg20  35481  cdlemg22  35483  cdlemg29  35501  cdlemg38  35511  cdlemk33N  35705  cdlemk56  35767