Theorem simpl11 1071

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpl11	|- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et ) -> ph )

Proof of Theorem simpl11

Step	Hyp	Ref	Expression
1		simp11 1026	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) -> ph )
2	1	adantr 465	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et ) -> ph )

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  14219  tsmsxp  20525  brbtwn2  24031  ax5seg  24064  br8  29112  btwndiff  29604  ifscgr  29621  seglecgr12im  29687  fourierdlem77  31807  lkrshp  34303  cvlcvr1  34537  atbtwn  34643  3dimlem3  34658  3dimlem3OLDN  34659  1cvratex  34670  llnmlplnN  34736  4atlem3  34793  4atlem3a  34794  4atlem11  34806  4atlem12  34809  lnatexN  34976  cdlemb  34991  paddasslem4  35020  paddasslem10  35026  pmodlem1  35043  llnexchb2lem  35065  llnexchb2  35066  arglem1N  35387  cdlemd4  35398  cdlemd9  35403  cdlemd  35404  cdleme16  35482  cdleme20  35521  cdleme21i  35532  cdleme21k  35535  cdleme27N  35566  cdleme28c  35569  cdlemefrs29bpre0  35593  cdlemefrs29clN  35596  cdlemefrs32fva  35597  cdleme41sn3a  35630  cdleme32fva  35634  cdleme40n  35665  cdlemg12e  35844  cdlemg15a  35852  cdlemg15  35853  cdlemg16ALTN  35855  cdlemg16z  35856  cdlemg20  35882  cdlemg22  35884  cdlemg29  35902  cdlemg38  35912  cdlemk33N  36106  cdlemk56  36168  dihord11b  36420  dihord2pre  36423  dihord4  36456