Theorem simpl12 1137

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

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:  pythagtriplem4  15524  pmatcollpw1lem1  20579  pmatcollpw1  20581  mp2pm2mplem2  20612  brbtwn2  25785  ax5seg  25818  3vfriswmgr  27142  br8  31646  nolt02o  31845  ifscgr  32151  seglecgr12im  32217  lkrshp  34392  atlatle  34607  cvlcvr1  34626  atbtwn  34732  3dimlem3  34747  3dimlem3OLDN  34748  1cvratex  34759  llnmlplnN  34825  4atlem3  34882  4atlem3a  34883  4atlem11  34895  4atlem12  34898  cdlemb  35080  paddasslem4  35109  paddasslem10  35115  pmodlem1  35132  llnexchb2lem  35154  arglem1N  35477  cdlemd4  35488  cdlemd  35494  cdleme16  35572  cdleme20  35612  cdleme21k  35626  cdleme22cN  35630  cdleme27N  35657  cdleme28c  35660  cdleme29ex  35662  cdleme32fva  35725  cdleme40n  35756  cdlemg15a  35943  cdlemg15  35944  cdlemg16ALTN  35946  cdlemg16z  35947  cdlemg20  35973  cdlemg22  35975  cdlemg29  35993  cdlemg38  36003  cdlemk33N  36197  cdlemk56  36259  fourierdlem77  40400