Theorem simp-6l 810

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)

Assertion

Ref	Expression
simp-6l	|- ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ph )

Proof of Theorem simp-6l

Step	Hyp	Ref	Expression
1		simp-5l 808	. 2 |- ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) -> ph )
2	1	adantr 481	1 |- ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ph )

Syntax hints:   -> wi 4   /\ wa 384

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

This theorem is referenced by:  simp-7l  812  ghmcmn  18237  ustuqtop2  22046  ustuqtop4  22048  cnheibor  22754  miriso  25565  f1otrg  25751  txomap  29901  pstmxmet  29940  omssubadd  30362  signstfvneq0  30649  iunconnlem2  39171  suplesup  39555  limcleqr  39876  0ellimcdiv  39881  limclner  39883  fourierdlem51  40374  smflimlem2  40980