Theorem simpl11 1032

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

Syntax hints:   -> wi 4   /\ wa 359   /\ w3a 936

This theorem is referenced by:  pythagtriplem4  13148  tsmsxp  18137  br8  25327  brbtwn2  25748  ax5seg  25781  btwndiff  25865  ifscgr  25882  seglecgr12im  25948  lkrshp  29588  cvlcvr1  29822  atbtwn  29928  3dimlem3  29943  3dimlem3OLDN  29944  1cvratex  29955  llnmlplnN  30021  4atlem3  30078  4atlem3a  30079  4atlem11  30091  4atlem12  30094  lnatexN  30261  cdlemb  30276  paddasslem4  30305  paddasslem10  30311  pmodlem1  30328  llnexchb2lem  30350  llnexchb2  30351  arglem1N  30672  cdlemd4  30683  cdlemd9  30688  cdlemd  30689  cdleme16  30767  cdleme20  30806  cdleme21i  30817  cdleme21k  30820  cdleme27N  30851  cdleme28c  30854  cdlemefrs29bpre0  30878  cdlemefrs29clN  30881  cdlemefrs32fva  30882  cdleme41sn3a  30915  cdleme32fva  30919  cdleme40n  30950  cdlemg12e  31129  cdlemg15a  31137  cdlemg15  31138  cdlemg16ALTN  31140  cdlemg16z  31141  cdlemg20  31167  cdlemg22  31169  cdlemg29  31187  cdlemg38  31197  cdlemk33N  31391  cdlemk56  31453  dihord11b  31705  dihord2pre  31708  dihord4  31741

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938