Theorem ad6antr 740

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 738	. 2 |- ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ps )
3	2	adantr 466	1 |- ( ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) -> ps )

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  ad7antr  742  catass  15543  funcpropd  15756  natpropd  15832  restutop  21183  utopreg  21198  restmetu  21516  lgamucov  23828  istrkgcb  24367  tgifscgr  24416  tgbtwnconn1lem3  24479  legtrd  24494  miriso  24574  footex  24620  opphllem3  24648  opphl  24653  trgcopy  24702  cgratr  24721  dfcgra2  24726  f1otrge  24748  cusgrares  25045  clwlkisclwwlklem1  25360  heicant  31682  mblfinlem3  31686  limclner  37307