Theorem ad6antr 772

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 770	. 2 |- ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ps )
3	2	adantr 481	1 |- ( ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) -> 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:  ad7antr  774  catass  16347  funcpropd  16560  natpropd  16636  restutop  22041  utopreg  22056  restmetu  22375  lgamucov  24764  istrkgcb  25355  tgifscgr  25403  tgbtwnconn1lem3  25469  legtrd  25484  miriso  25565  footex  25613  opphllem3  25641  opphl  25646  trgcopy  25696  cgratr  25715  dfcgra2  25721  inaghl  25731  cgrg3col4  25734  f1otrge  25752  clwlkclwwlklem2  26901  matunitlindflem1  33405  heicant  33444  mblfinlem3  33448  limclner  39883  hoidmvle  40814