Theorem simpl11 1063

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 1018	. 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 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  14008  tsmsxp  19871  brbtwn2  23330  ax5seg  23363  br8  27733  btwndiff  28225  ifscgr  28242  seglecgr12im  28308  lkrshp  33113  cvlcvr1  33347  atbtwn  33453  3dimlem3  33468  3dimlem3OLDN  33469  1cvratex  33480  llnmlplnN  33546  4atlem3  33603  4atlem3a  33604  4atlem11  33616  4atlem12  33619  lnatexN  33786  cdlemb  33801  paddasslem4  33830  paddasslem10  33836  pmodlem1  33853  llnexchb2lem  33875  llnexchb2  33876  arglem1N  34197  cdlemd4  34208  cdlemd9  34213  cdlemd  34214  cdleme16  34292  cdleme20  34331  cdleme21i  34342  cdleme21k  34345  cdleme27N  34376  cdleme28c  34379  cdlemefrs29bpre0  34403  cdlemefrs29clN  34406  cdlemefrs32fva  34407  cdleme41sn3a  34440  cdleme32fva  34444  cdleme40n  34475  cdlemg12e  34654  cdlemg15a  34662  cdlemg15  34663  cdlemg16ALTN  34665  cdlemg16z  34666  cdlemg20  34692  cdlemg22  34694  cdlemg29  34712  cdlemg38  34722  cdlemk33N  34916  cdlemk56  34978  dihord11b  35230  dihord2pre  35233  dihord4  35266