Theorem ad6antr 735

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

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  ad7antr  737  catass  14941  funcpropd  15127  natpropd  15203  restutop  20503  utopreg  20518  restmetu  20853  tgifscgr  23656  tgcgrxfr  23665  tgbtwnconn1lem3  23716  legtrd  23731  miriso  23791  footex  23831  mideulem  23841  f1otrge  23879  cusgrares  24176  clwlkisclwwlklem1  24491  lgamucov  28248  heicant  29654  mblfinlem3  29658  limclner  31221