Theorem simpl11 1069

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

Syntax hints:   -> wi 4   /\ wa 367   /\ w3a 971

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 369  df-3an 973

This theorem is referenced by:  pythagtriplem4  14430  tsmsxp  20826  brbtwn2  24413  ax5seg  24446  br8  29429  btwndiff  29908  ifscgr  29925  seglecgr12im  29991  fourierdlem77  32208  lkrshp  35246  cvlcvr1  35480  atbtwn  35586  3dimlem3  35601  3dimlem3OLDN  35602  1cvratex  35613  llnmlplnN  35679  4atlem3  35736  4atlem3a  35737  4atlem11  35749  4atlem12  35752  lnatexN  35919  cdlemb  35934  paddasslem4  35963  paddasslem10  35969  pmodlem1  35986  llnexchb2lem  36008  llnexchb2  36009  arglem1N  36331  cdlemd4  36342  cdlemd9  36347  cdlemd  36348  cdleme16  36426  cdleme20  36466  cdleme21i  36477  cdleme21k  36480  cdleme27N  36511  cdleme28c  36514  cdlemefrs29bpre0  36538  cdlemefrs29clN  36541  cdlemefrs32fva  36542  cdleme41sn3a  36575  cdleme32fva  36579  cdleme40n  36610  cdlemg12e  36789  cdlemg15a  36797  cdlemg15  36798  cdlemg16ALTN  36800  cdlemg16z  36801  cdlemg20  36827  cdlemg22  36829  cdlemg29  36847  cdlemg38  36857  cdlemk33N  37051  cdlemk56  37113  dihord11b  37365  dihord2pre  37368  dihord4  37401