Theorem simpl11 1083

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

Syntax hints:   -> wi 4   /\ wa 371   /\ w3a 985

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 189  df-an 373  df-3an 987

This theorem is referenced by:  pythagtriplem4  14769  tsmsxp  21169  brbtwn2  24935  ax5seg  24968  br8  30396  btwndiff  30794  ifscgr  30811  seglecgr12im  30877  lkrshp  32671  cvlcvr1  32905  atbtwn  33011  3dimlem3  33026  3dimlem3OLDN  33027  1cvratex  33038  llnmlplnN  33104  4atlem3  33161  4atlem3a  33162  4atlem11  33174  4atlem12  33177  lnatexN  33344  cdlemb  33359  paddasslem4  33388  paddasslem10  33394  pmodlem1  33411  llnexchb2lem  33433  llnexchb2  33434  arglem1N  33756  cdlemd4  33767  cdlemd9  33772  cdlemd  33773  cdleme16  33851  cdleme20  33891  cdleme21i  33902  cdleme21k  33905  cdleme27N  33936  cdleme28c  33939  cdlemefrs29bpre0  33963  cdlemefrs29clN  33966  cdlemefrs32fva  33967  cdleme41sn3a  34000  cdleme32fva  34004  cdleme40n  34035  cdlemg12e  34214  cdlemg15a  34222  cdlemg15  34223  cdlemg16ALTN  34225  cdlemg16z  34226  cdlemg20  34252  cdlemg22  34254  cdlemg29  34272  cdlemg38  34282  cdlemk33N  34476  cdlemk56  34538  dihord11b  34790  dihord2pre  34793  dihord4  34826  fourierdlem77  38047