Theorem simp-6r 811

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

Assertion

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

Proof of Theorem simp-6r

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

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-7r  813  catass  16347  mhmmnd  17537  scmatscm  20319  cfilucfil  22364  istrkgb  25354  istrkge  25356  tgbtwnconn1  25470  legso  25494  footex  25613  opphl  25646  trgcopy  25696  dfcgra2  25721  cgrg3col4  25734  f1otrg  25751  2sqmo  29649  pstmxmet  29940  signstfvneq0  30649  afsval  30749  mblfinlem3  33448  mblfinlem4  33449  iunconnlem2  39171  suplesup  39555  limclner  39883  fourierdlem51  40374  hoidmvle  40814  smfmullem3  41000