Theorem simpl11 1080

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

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  pythagtriplem4  14732  tsmsxp  21100  brbtwn2  24781  ax5seg  24814  br8  30183  btwndiff  30579  ifscgr  30596  seglecgr12im  30662  lkrshp  32379  cvlcvr1  32613  atbtwn  32719  3dimlem3  32734  3dimlem3OLDN  32735  1cvratex  32746  llnmlplnN  32812  4atlem3  32869  4atlem3a  32870  4atlem11  32882  4atlem12  32885  lnatexN  33052  cdlemb  33067  paddasslem4  33096  paddasslem10  33102  pmodlem1  33119  llnexchb2lem  33141  llnexchb2  33142  arglem1N  33464  cdlemd4  33475  cdlemd9  33480  cdlemd  33481  cdleme16  33559  cdleme20  33599  cdleme21i  33610  cdleme21k  33613  cdleme27N  33644  cdleme28c  33647  cdlemefrs29bpre0  33671  cdlemefrs29clN  33674  cdlemefrs32fva  33675  cdleme41sn3a  33708  cdleme32fva  33712  cdleme40n  33743  cdlemg12e  33922  cdlemg15a  33930  cdlemg15  33931  cdlemg16ALTN  33933  cdlemg16z  33934  cdlemg20  33960  cdlemg22  33962  cdlemg29  33980  cdlemg38  33990  cdlemk33N  34184  cdlemk56  34246  dihord11b  34498  dihord2pre  34501  dihord4  34534  fourierdlem77  37614