Theorem simpl12 1070

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

Syntax hints:   -> wi 4   /\ wa 367   /\ w3a 971

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 369  df-3an 973

This theorem is referenced by:  pythagtriplem4  14345  pmatcollpw1lem1  19360  pmatcollpw1  19362  mp2pm2mplem2  19393  brbtwn2  24329  ax5seg  24362  br8  29351  ifscgr  29847  seglecgr12im  29913  fourierdlem77  32132  lkrshp  35243  atlatle  35458  cvlcvr1  35477  atbtwn  35583  3dimlem3  35598  3dimlem3OLDN  35599  1cvratex  35610  llnmlplnN  35676  4atlem3  35733  4atlem3a  35734  4atlem11  35746  4atlem12  35749  cdlemb  35931  paddasslem4  35960  paddasslem10  35966  pmodlem1  35983  llnexchb2lem  36005  arglem1N  36328  cdlemd4  36339  cdlemd  36345  cdleme16  36423  cdleme20  36463  cdleme21k  36477  cdleme22cN  36481  cdleme27N  36508  cdleme28c  36511  cdleme29ex  36513  cdleme32fva  36576  cdleme40n  36607  cdlemg15a  36794  cdlemg15  36795  cdlemg16ALTN  36797  cdlemg16z  36798  cdlemg20  36824  cdlemg22  36826  cdlemg29  36844  cdlemg38  36854  cdlemk33N  37048  cdlemk56  37110