Theorem simp1l1 1154

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp1l1	|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta /\ et ) -> ph )

Proof of Theorem simp1l1

Step	Hyp	Ref	Expression
1		simpl1 1064	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ph )
2	1	3ad2ant1 1082	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta /\ et ) -> ph )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  mapxpen  8126  lsmcv  19141  archiabl  29752  trisegint  32135  linethru  32260  hlrelat3  34698  cvrval3  34699  cvrval4N  34700  2atlt  34725  atbtwnex  34734  1cvratlt  34760  atcvrlln2  34805  atcvrlln  34806  2llnmat  34810  lplnexllnN  34850  lvolnlelpln  34871  lnjatN  35066  lncvrat  35068  lncmp  35069  cdlemd9  35493  dihord5b  36548  dihmeetALTN  36616  dih1dimatlem0  36617  mapdrvallem2  36934