Theorem simpl12 1064

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 1019	. 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 965

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 967

This theorem is referenced by:  pythagtriplem4  14005  brbtwn2  23304  ax5seg  23337  br8  27711  ifscgr  28220  seglecgr12im  28286  pmatcollpw1lem1  31262  pmatcollpw1  31264  mp2pm2mplem2  31295  lkrshp  33089  atlatle  33304  cvlcvr1  33323  atbtwn  33429  3dimlem3  33444  3dimlem3OLDN  33445  1cvratex  33456  llnmlplnN  33522  4atlem3  33579  4atlem3a  33580  4atlem11  33592  4atlem12  33595  cdlemb  33777  paddasslem4  33806  paddasslem10  33812  pmodlem1  33829  llnexchb2lem  33851  arglem1N  34173  cdlemd4  34184  cdlemd  34190  cdleme16  34268  cdleme20  34307  cdleme21k  34321  cdleme22cN  34325  cdleme27N  34352  cdleme28c  34355  cdleme29ex  34357  cdleme32fva  34420  cdleme40n  34451  cdlemg15a  34638  cdlemg15  34639  cdlemg16ALTN  34641  cdlemg16z  34642  cdlemg20  34668  cdlemg22  34670  cdlemg29  34688  cdlemg38  34698  cdlemk33N  34892  cdlemk56  34954