Theorem simpl11 1058

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

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 960

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 962

This theorem is referenced by:  pythagtriplem4  13882  tsmsxp  19629  brbtwn2  23070  ax5seg  23103  br8  27479  btwndiff  27971  ifscgr  27988  seglecgr12im  28054  lkrshp  32438  cvlcvr1  32672  atbtwn  32778  3dimlem3  32793  3dimlem3OLDN  32794  1cvratex  32805  llnmlplnN  32871  4atlem3  32928  4atlem3a  32929  4atlem11  32941  4atlem12  32944  lnatexN  33111  cdlemb  33126  paddasslem4  33155  paddasslem10  33161  pmodlem1  33178  llnexchb2lem  33200  llnexchb2  33201  arglem1N  33522  cdlemd4  33533  cdlemd9  33538  cdlemd  33539  cdleme16  33617  cdleme20  33656  cdleme21i  33667  cdleme21k  33670  cdleme27N  33701  cdleme28c  33704  cdlemefrs29bpre0  33728  cdlemefrs29clN  33731  cdlemefrs32fva  33732  cdleme41sn3a  33765  cdleme32fva  33769  cdleme40n  33800  cdlemg12e  33979  cdlemg15a  33987  cdlemg15  33988  cdlemg16ALTN  33990  cdlemg16z  33991  cdlemg20  34017  cdlemg22  34019  cdlemg29  34037  cdlemg38  34047  cdlemk33N  34241  cdlemk56  34303  dihord11b  34555  dihord2pre  34558  dihord4  34591