Theorem ad6antr 747

Description: Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)

Hypothesis

Ref	Expression
ad2ant.1	|- ( ph -> ps )

Assertion

Ref	Expression
ad6antr	|- ( ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) -> ps )

Proof of Theorem ad6antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	ad5antr 745	. 2 |- ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ps )
3	2	adantr 471	1 |- ( ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) -> ps )

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  ad7antr  749  catass  15641  funcpropd  15854  natpropd  15930  restutop  21301  utopreg  21316  restmetu  21634  lgamucov  24012  istrkgcb  24553  tgifscgr  24602  tgbtwnconn1lem3  24668  legtrd  24683  miriso  24764  footex  24812  opphllem3  24840  opphl  24845  trgcopy  24895  cgratr  24914  dfcgra2  24920  inaghl  24930  cgrg3col4  24933  f1otrge  24951  cusgrares  25249  clwlkisclwwlklem1  25564  heicant  32020  mblfinlem3  32024  limclner  37770  hoidmvle  38460